-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 :
+ ?where:ProofEngineTypes.pattern ->
+ term:Cic.term -> unit -> ProofEngineTypes.tactic
+val rewrite_back :
+ ?where:ProofEngineTypes.pattern ->
+ term:Cic.term -> unit -> ProofEngineTypes.tactic
+val rewrite_back_simpl :
+ ?where:ProofEngineTypes.pattern ->
+ term:Cic.term -> unit -> ProofEngineTypes.tactic
+val rewrite_simpl :
+ ?where:ProofEngineTypes.pattern ->
+ term:Cic.term -> unit -> ProofEngineTypes.tactic