-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.lazy_pattern ->
+ with_what:Cic.lazy_term -> ProofEngineTypes.tactic
+val rewrite :
+ direction:[ `LeftToRight | `RightToLeft ] ->
+ pattern:ProofEngineTypes.lazy_pattern ->
+ Cic.term -> ProofEngineTypes.tactic
+val rewrite_simpl :
+ direction:[ `LeftToRight | `RightToLeft ] ->
+ pattern:ProofEngineTypes.lazy_pattern ->
+ Cic.term -> ProofEngineTypes.tactic