attributes now in the proof status: commit 4

[helm.git] / matita / matita.ml

diff --git a/matita/matita.ml b/matita/matita.ml
index 5a638b48d79bb86fd39188b0c9cbe753aead9e63..46926ea9b387e75a32d0d9c213030136459485d2 100644 (file)
--- a/matita/matita.ml
+++ b/matita/matita.ml
@@ -167,8 +167,8 @@ let _ =
             (MatitaScript.current ())#grafite_status.GrafiteTypes.proof_status
             with
             | GrafiteTypes.No_proof -> (Cic.Implicit None)
-            | Incomplete_proof i -> let _,_,p,_ = i.GrafiteTypes.proof in p
-            | Proof p -> let _,_,p,_ = p in p
+            | Incomplete_proof i -> let _,_,p,_, _ = i.GrafiteTypes.proof in p
+            | Proof p -> let _,_,p,_, _ = p in p
             | Intermediate _ -> assert false)));
      addDebugItem "Print current proof (natural language) to stderr" 
        (fun _ -> 
@@ -179,10 +179,10 @@ let _ =
             with
             | GrafiteTypes.No_proof -> assert false
             | Incomplete_proof i -> 
-                let _,m,p,ty = i.GrafiteTypes.proof in 
-                Cic.CurrentProof ("current (incomplete) proof",m,p,ty,[],[])
-            | Proof (_,m,p,ty) -> 
-                Cic.CurrentProof ("current proof",m,p,ty,[],[])
+                let _,m,p,ty, attrs = i.GrafiteTypes.proof in 
+                Cic.CurrentProof ("current (incomplete) proof",m,p,ty,[],attrs)
+            | Proof (_,m,p,ty, attrs) -> 
+                Cic.CurrentProof ("current proof",m,p,ty,[],attrs)
             | Intermediate _ -> assert false)));
 (*     addDebugItem "ask record choice"
       (fun _ ->