added a (for the moment) dummy field _subst to ProofengineTypes.proof.

[helm.git] / components / tactics / statefulProofEngine.ml

diff --git a/components/tactics/statefulProofEngine.ml b/components/tactics/statefulProofEngine.ml
index 4e3badea4781e97f3595235971590e21eddae451..37800187ad4d290fb5c3bba38b9f53b78355c6b6 100644 (file)
--- a/components/tactics/statefulProofEngine.ml
+++ b/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 =