X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2FstatefulProofEngine.ml;h=37800187ad4d290fb5c3bba38b9f53b78355c6b6;hb=7cb22a7f8107a6cde0b77b7879e04f586a347102;hp=4e3badea4781e97f3595235971590e21eddae451;hpb=61a2faa2694907757dd617175e0144705e79d65a;p=helm.git

diff --git a/helm/software/components/tactics/statefulProofEngine.ml b/helm/software/components/tactics/statefulProofEngine.ml
index 4e3badea4..37800187a 100644
--- a/helm/software/components/tactics/statefulProofEngine.ml
+++ b/helm/software/components/tactics/statefulProofEngine.ml
@@ -52,11 +52,12 @@ class ['a] status
       incr next_id;
       !next_id
   in
-  let initial_proof = ((uri: UriManager.uri option), metasenv, body, typ, attrs) in
+  let _subst = ([] : Cic.substitution) in
+  let initial_proof = ((uri: UriManager.uri option), metasenv, _subst, body, typ, attrs) in
   let next_goal (goals, proof) =
     match goals, proof with
     | goal :: _, _ -> Some goal
-    | [], (_, (goal, _, _) :: _, _, _, _) ->
+    | [], (_, (goal, _, _) :: _, _, _, _, _) ->
         (* the tactic left no open goal: let's choose the first open goal *)
         Some goal
     | _, _ -> None
@@ -109,24 +110,24 @@ class ['a] status
         raise exn
 *)
 
-    method uri      = let (uri, _, _, _, _)      = _proof in uri
-    method metasenv = let (_, metasenv, _, _, _) = _proof in metasenv
-    method body     = let (_, _, body, _, _)     = _proof in body
-    method typ      = let (_, _, _, typ, _)      = _proof in typ
-    method attrs    = let (_, _, _, _, attrs)    = _proof in attrs
+    method uri      = let (uri, _, _, _, _, _)      = _proof in uri
+    method metasenv = let (_, metasenv, _, _, _, _) = _proof in metasenv
+    method body     = let (_, _, _, body, _, _)     = _proof in body
+    method typ      = let (_, _, _, _, typ, _)      = _proof in typ
+    method attrs    = let (_, _, _, _, _, attrs)    = _proof in attrs
 
     method set_metasenv metasenv =
-      let (uri, _, body, typ, attes) = _proof in
-      _proof <- (uri, metasenv, body, typ, attrs)
+      let (uri, _,  _subst,body, typ, attes) = _proof in
+      _proof <- (uri, metasenv,  _subst,body, typ, attrs)
 
     method set_uri uri =
-      let (old_uri, metasenv, body, typ, attrs) = _proof in
+      let (old_uri, metasenv,  _subst,body, typ, attrs) = _proof in
       if old_uri <> None then
         raise Uri_redefinition;
-      _proof <- (Some uri, metasenv, body, typ, attrs)
+      _proof <- (Some uri, metasenv,  _subst,body, typ, attrs)
 
     method conjecture goal =
-      let (_, metasenv, _, _, _) = _proof in
+      let (_, metasenv, _subst, _, _, _) = _proof in
       CicUtil.lookup_meta goal metasenv
 
     method apply_tactic tactic =