]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/tactics/equalityTactics.mli
added support for repository attributes
[helm.git] / helm / ocaml / tactics / equalityTactics.mli
index d156ae440d0199940fa8f8b0d47e849c8f74e759..1d60ae149676d23c129e64a043026d746b1c2d90 100644 (file)
  *)
 
 val rewrite_tac: 
-  ?where:ProofEngineTypes.pattern -> 
-  term:Cic.term -> unit -> ProofEngineTypes.tactic
+  direction:[`LeftToRight | `RightToLeft] ->
+  pattern:ProofEngineTypes.lazy_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.lazy_pattern -> Cic.term -> ProofEngineTypes.tactic
   
 val replace_tac: 
-  pattern:ProofEngineTypes.pattern ->
-  with_what:Cic.term -> ProofEngineTypes.tactic
+  pattern:ProofEngineTypes.lazy_pattern ->
+  with_what:Cic.lazy_term -> ProofEngineTypes.tactic
 
 val reflexivity_tac: ProofEngineTypes.tactic
 val symmetry_tac: ProofEngineTypes.tactic