parameter sintax added to axiom statement

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

diff --git a/helm/software/components/tactics/statefulProofEngine.ml b/helm/software/components/tactics/statefulProofEngine.ml
index 9529c897c9362a214a7e88c559dc407b992b0667..37800187ad4d290fb5c3bba38b9f53b78355c6b6 100644 (file)
--- a/helm/software/components/tactics/statefulProofEngine.ml
+++ b/helm/software/components/tactics/statefulProofEngine.ml
@@ -44,7 +44,7 @@ exception Data_failure of exn
 
 class ['a] status
   ?(history_size = default_history_size)
-  ?uri ~typ ~body ~metasenv init_data compute_data ()
+  ?uri ~typ ~body ~metasenv ~attrs init_data compute_data ()
   =
   let next_observer_id =
     let next_id = ref 0 in
@@ -52,11 +52,12 @@ class ['a] status
       incr next_id;
       !next_id
   in
-  let initial_proof = ((uri: UriManager.uri option), metasenv, body, typ) 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,23 +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 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) = _proof in
-      _proof <- (uri, metasenv, body, typ)
+      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) = _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)
+      _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 =
@@ -209,6 +211,6 @@ class ['a] status
 
   end
 
-let trivial_status ?uri ~typ ~body ~metasenv () =
-  new status ?uri ~typ ~body ~metasenv (fun _ -> ()) (fun _ _ -> ()) ()
+let trivial_status ?uri ~typ ~body ~metasenv ~attrs () =
+  new status ?uri ~typ ~body ~metasenv ~attrs (fun _ -> ()) (fun _ _ -> ()) ()