-val replace : what:Cic.term -> with_what:Cic.term -> ProofEngineTypes.tactic
-val rewrite_back : term:Cic.term -> ProofEngineTypes.tactic
-val rewrite_back_simpl : term:Cic.term -> ProofEngineTypes.tactic
-val rewrite : term:Cic.term -> ProofEngineTypes.tactic
-val rewrite_simpl : term:Cic.term -> ProofEngineTypes.tactic
+val replace :
+ pattern:ProofEngineTypes.pattern ->
+ with_what:Cic.term -> ProofEngineTypes.tactic
+val rewrite :
+ direction:[ `LeftToRight | `RightToLeft ] ->
+ pattern:ProofEngineTypes.pattern -> Cic.term -> ProofEngineTypes.tactic
+val rewrite_simpl :
+ direction:[ `LeftToRight | `RightToLeft ] ->
+ pattern:ProofEngineTypes.pattern -> Cic.term -> ProofEngineTypes.tactic