X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2FproofEngineTypes.ml;h=c60b6fdc0080ae6fbbecfa238a2c215267d31c83;hb=82baf094141d9ef518d681b8cebcc180bca14d2c;hp=93436e799586b899ecd4ffe6a7ebb098e8e3f5b0;hpb=18825eb46860edafe9b1082b2ed4c679778a4ce8;p=helm.git

diff --git a/helm/software/components/tactics/proofEngineTypes.ml b/helm/software/components/tactics/proofEngineTypes.ml
index 93436e799..c60b6fdc0 100644
--- a/helm/software/components/tactics/proofEngineTypes.ml
+++ b/helm/software/components/tactics/proofEngineTypes.ml
@@ -28,7 +28,8 @@
   (**
     current proof (proof uri * metas * (in)complete proof * term to be prooved)
   *)
-type proof = UriManager.uri option * Cic.metasenv * Cic.substitution * Cic.term * Cic.term * Cic.attribute list
+type proof = 
+  UriManager.uri option * Cic.metasenv * Cic.substitution * Cic.term Lazy.t * Cic.term * Cic.attribute list
   (** current goal, integer index *)
 type goal = int
 type status = proof * goal
@@ -45,7 +46,8 @@ let initial_status ty metasenv attrs =
   let newmeta_idx = aux 0 metasenv in
   let _subst = [] in
   let proof =
-    None, (newmeta_idx, [], ty) :: metasenv, _subst, Cic.Meta (newmeta_idx, []), ty, attrs
+    None, (newmeta_idx, [], ty) :: metasenv, _subst, 
+    lazy (Cic.Meta (newmeta_idx, [])), ty, attrs
   in
   (proof, newmeta_idx)