X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Focaml%2Ftactics%2Ftactics.mli;h=5ac63b07e9696310af3736cfa367cde902240fd0;hb=a93a94942ad58d8645af1fd94bef8fa31d9541a4;hp=77e3f8ac545f176a1ac99488be6df6607bbf847f;hpb=6531c263da005e25ea2f58f9ee960acba7857ff6;p=helm.git

diff --git a/helm/ocaml/tactics/tactics.mli b/helm/ocaml/tactics/tactics.mli
index 77e3f8ac5..5ac63b07e 100644
--- a/helm/ocaml/tactics/tactics.mli
+++ b/helm/ocaml/tactics/tactics.mli
@@ -7,7 +7,8 @@ val auto :
   ?width:int ->
   ?paramodulation:string -> dbd:Mysql.dbd -> unit -> ProofEngineTypes.tactic
 val change :
-  pattern:ProofEngineTypes.pattern -> Cic.term -> ProofEngineTypes.tactic
+  pattern:ProofEngineTypes.pattern ->
+  ProofEngineTypes.lazy_term -> ProofEngineTypes.tactic
 val clear : hyp:string -> ProofEngineTypes.tactic
 val clearbody : hyp:string -> ProofEngineTypes.tactic
 val compare : term:Cic.term -> ProofEngineTypes.tactic
@@ -35,8 +36,8 @@ val exact : term:Cic.term -> ProofEngineTypes.tactic
 val exists : ProofEngineTypes.tactic
 val fail : ProofEngineTypes.tactic
 val fold :
-  reduction:(Cic.context -> Cic.term -> Cic.term) ->
-  term:Cic.term ->
+  reduction:ProofEngineTypes.lazy_reduction ->
+  term:ProofEngineTypes.lazy_term ->
   pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic
 val fourier : ProofEngineTypes.tactic
 val fwd_simpl :
@@ -64,7 +65,7 @@ val reduce : pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic
 val reflexivity : ProofEngineTypes.tactic
 val replace :
   pattern:ProofEngineTypes.pattern ->
-  with_what:Cic.term -> ProofEngineTypes.tactic
+  with_what:ProofEngineTypes.lazy_term -> ProofEngineTypes.tactic
 val rewrite :
   direction:[ `LeftToRight | `RightToLeft ] ->
   pattern:ProofEngineTypes.pattern -> Cic.term -> ProofEngineTypes.tactic
@@ -79,6 +80,6 @@ val split : ProofEngineTypes.tactic
 val symmetry : ProofEngineTypes.tactic
 val transitivity : term:Cic.term -> ProofEngineTypes.tactic
 val unfold :
-  Cic.term option ->
+  ProofEngineTypes.lazy_term option ->
   pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic
 val whd : pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic