X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=components%2Ftactics%2FstatefulProofEngine.mli;h=64a394d744bc23dbad51af14c1f8111171eb4ef4;hb=refs%2Ftags%2F0.4.95%407852;hp=4198876ca239b4e191395fbac58efc788b0801d9;hpb=7f2444c2670cadafddd8785b687ef312158376b0;p=helm.git

diff --git a/components/tactics/statefulProofEngine.mli b/components/tactics/statefulProofEngine.mli
index 4198876ca..64a394d74 100644
--- a/components/tactics/statefulProofEngine.mli
+++ b/components/tactics/statefulProofEngine.mli
@@ -63,6 +63,7 @@ class ['a] status:
   ?history_size:int ->  (** default 20 *)
   ?uri:UriManager.uri ->
   typ:Cic.term -> body:Cic.term -> metasenv:Cic.metasenv ->
+  attrs:Cic.attribute list ->
   (proof_status -> 'a) -> (* init data *)
   (proof_status * 'a -> proof_status -> 'a) ->  (* update data *)
   unit ->
@@ -72,6 +73,7 @@ class ['a] status:
     method metasenv: Cic.metasenv
     method body: Cic.term
     method typ: Cic.term
+    method attrs: Cic.attribute list
 
     (** change metasenv _without_ triggering any notification *)
     method set_metasenv: Cic.metasenv -> unit
@@ -115,6 +117,7 @@ class ['a] status:
 val trivial_status:
   ?uri:UriManager.uri ->
   typ:Cic.term -> body:Cic.term -> metasenv:Cic.metasenv ->
+  attrs:Cic.attribute list ->
   unit ->
     unit status