- ?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
+ direction:[ `LeftToRight | `RightToLeft ] ->
+ pattern:ProofEngineTypes.lazy_pattern ->
+ Cic.term -> ProofEngineTypes.tactic