X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2FstatefulProofEngine.mli;h=06defd79fcead87272be0850c48ad067679c5de1;hb=f9abd21eb0d26cf9b632af4df819225be4d091e3;hp=64a394d744bc23dbad51af14c1f8111171eb4ef4;hpb=61a2faa2694907757dd617175e0144705e79d65a;p=helm.git

diff --git a/helm/software/components/tactics/statefulProofEngine.mli b/helm/software/components/tactics/statefulProofEngine.mli
index 64a394d74..06defd79f 100644
--- a/helm/software/components/tactics/statefulProofEngine.mli
+++ b/helm/software/components/tactics/statefulProofEngine.mli
@@ -62,7 +62,7 @@ exception Data_failure of exn
 class ['a] status:
   ?history_size:int ->  (** default 20 *)
   ?uri:UriManager.uri ->
-  typ:Cic.term -> body:Cic.term -> metasenv:Cic.metasenv ->
+  typ:Cic.term -> body:Cic.term Lazy.t -> metasenv:Cic.metasenv ->
   attrs:Cic.attribute list ->
   (proof_status -> 'a) -> (* init data *)
   (proof_status * 'a -> proof_status -> 'a) ->  (* update data *)
@@ -71,7 +71,7 @@ class ['a] status:
 
     method proof: ProofEngineTypes.proof
     method metasenv: Cic.metasenv
-    method body: Cic.term
+    method body: Cic.term Lazy.t
     method typ: Cic.term
     method attrs: Cic.attribute list
 
@@ -116,7 +116,7 @@ class ['a] status:
 
 val trivial_status:
   ?uri:UriManager.uri ->
-  typ:Cic.term -> body:Cic.term -> metasenv:Cic.metasenv ->
+  typ:Cic.term -> body:Cic.term Lazy.t -> metasenv:Cic.metasenv ->
   attrs:Cic.attribute list ->
   unit ->
     unit status