librarian.ml: now the read_only .moo's are managed "correctly" (i.e. better than...

[helm.git] / helm / software / matita / matita.ml

diff --git a/helm/software/matita/matita.ml b/helm/software/matita/matita.ml
index 62e425bf38b13dcb28fc0c7f7e7e553d97d113bb..d63e327f03b89e8d68a58b7ce2a80e68e945ff78 100644 (file)
--- a/helm/software/matita/matita.ml
+++ b/helm/software/matita/matita.ml
@@ -116,6 +116,9 @@ let _ =
     let addDebugSeparator () =
       ignore (GMenu.separator_item ~packing:gui#main#debugMenu_menu#append ())
     in
+    addDebugItem "dump aliases" (fun _ ->
+      let status = script#lexicon_status in
+      HLog.debug (DisambiguatePp.pp_environment status.LexiconEngine.aliases));
     addDebugItem "dump environment to \"env.dump\"" (fun _ ->
       let oc = open_out "env.dump" in
       CicEnvironment.dump_to_channel oc;
@@ -168,8 +171,10 @@ let _ =
             (MatitaScript.current ())#grafite_status.GrafiteTypes.proof_status
             with
             | GrafiteTypes.No_proof -> (Cic.Implicit None)
-            | Incomplete_proof i -> let _,_,_subst,p,_, _ = i.GrafiteTypes.proof in p
-            | Proof p -> let _,_,_subst,p,_, _ = p in p
+            | Incomplete_proof i -> 
+                 let _,_,_subst,p,_, _ = i.GrafiteTypes.proof in 
+                 Lazy.force p
+            | Proof p -> let _,_,_subst,p,_, _ = p in Lazy.force p
             | Intermediate _ -> assert false)));
      addDebugItem "Print current proof (natural language) to stderr" 
        (fun _ -> 
@@ -183,9 +188,9 @@ let _ =
             | GrafiteTypes.No_proof -> assert false
             | Incomplete_proof i -> 
                 let _,m,_subst,p,ty, attrs = i.GrafiteTypes.proof in 
-                Cic.CurrentProof ("current (incomplete) proof",m,p,ty,[],attrs)
+                Cic.CurrentProof ("current (incomplete) proof",m,Lazy.force p,ty,[],attrs)
             | Proof (_,m,_subst,p,ty, attrs) -> 
-                Cic.CurrentProof ("current proof",m,p,ty,[],attrs)
+                Cic.CurrentProof ("current proof",m,Lazy.force p,ty,[],attrs)
             | Intermediate _ -> assert false)));
 (*     addDebugItem "ask record choice"
       (fun _ ->