package coq-waterproof

  1. Overview
  2. Docs

Generalization of tactics defined in coq-core for Mergeable-typed tactics

Parameters

module M : Mergeable

Signature

Merge of tactics' returned elements

val typedLongThen : M.elt Proofview.tactic list -> M.elt Proofview.tactic

Same as typedThen with a list of tactics

val typedIndependant : M.elt Proofview.tactic -> M.elt Proofview.tactic

Generalisation of Proofview.tclINDEPENDENT

OCaml

Innovation. Community. Security.