val rewrite_tac:
direction:[`LeftToRight | `RightToLeft] ->
- pattern:ProofEngineTypes.lazy_pattern -> Cic.term -> ProofEngineTypes.tactic
+ pattern:ProofEngineTypes.lazy_pattern -> Cic.term -> string list ->
+ ProofEngineTypes.tactic
val rewrite_simpl_tac:
direction:[`LeftToRight | `RightToLeft] ->
- pattern:ProofEngineTypes.lazy_pattern -> Cic.term -> ProofEngineTypes.tactic
+ pattern:ProofEngineTypes.lazy_pattern -> Cic.term -> string list ->
+ ProofEngineTypes.tactic
val replace_tac:
pattern:ProofEngineTypes.lazy_pattern ->
val reflexivity_tac: ProofEngineTypes.tactic
val symmetry_tac: ProofEngineTypes.tactic
val transitivity_tac: term:Cic.term -> ProofEngineTypes.tactic
-
-(* FG *)
-
-val subst_tac: hyp:string -> ProofEngineTypes.tactic