*)
val rewrite_tac:
- ?where:ProofEngineTypes.pattern ->
- term:Cic.term -> unit -> ProofEngineTypes.tactic
+ direction:[`LeftToRight | `RightToLeft] ->
+ pattern:ProofEngineTypes.pattern -> Cic.term -> ProofEngineTypes.tactic
val rewrite_simpl_tac:
- ?where:ProofEngineTypes.pattern ->
- term:Cic.term -> unit -> ProofEngineTypes.tactic
-val rewrite_back_tac:
- ?where:ProofEngineTypes.pattern ->
- term:Cic.term -> unit -> ProofEngineTypes.tactic
-val rewrite_back_simpl_tac:
- ?where:ProofEngineTypes.pattern ->
- term:Cic.term -> unit -> ProofEngineTypes.tactic
+ direction:[`LeftToRight | `RightToLeft] ->
+ pattern:ProofEngineTypes.pattern -> Cic.term -> ProofEngineTypes.tactic
val replace_tac:
- what:Cic.term -> with_what:Cic.term -> ProofEngineTypes.tactic
+ pattern:ProofEngineTypes.pattern ->
+ with_what:Cic.term -> ProofEngineTypes.tactic
val reflexivity_tac: ProofEngineTypes.tactic
val symmetry_tac: ProofEngineTypes.tactic