X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fmatita.ml;h=46926ea9b387e75a32d0d9c213030136459485d2;hb=e465656be7e67ee3c02acf12a53c8388ae384b0a;hp=5a638b48d79bb86fd39188b0c9cbe753aead9e63;hpb=34259adcd8a36e85f3224c7074c74aef878f1856;p=helm.git

diff --git a/helm/software/matita/matita.ml b/helm/software/matita/matita.ml
index 5a638b48d..46926ea9b 100644
--- a/helm/software/matita/matita.ml
+++ b/helm/software/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 _ ->