X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita.ml;h=a326754dc40a39ac65ad30df18e795f4d64eae95;hb=1776f357e1a69fa1133956660b65d7bafdfe5c25;hp=5df8656cdbb4cdbdffb930971c2ea4a0b19210ff;hpb=a1c4c601850c71e094a4703af00f02ca2026d8ed;p=helm.git

diff --git a/matita/matita.ml b/matita/matita.ml
index 5df8656cd..a326754dc 100644
--- a/matita/matita.ml
+++ b/matita/matita.ml
@@ -167,21 +167,23 @@ 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 _,_,_subst,p,_, _ = i.GrafiteTypes.proof in p
+            | Proof p -> let _,_,_subst,p,_, _ = p in p
             | Intermediate _ -> assert false)));
      addDebugItem "Print current proof (natural language) to stderr" 
        (fun _ -> 
         prerr_endline 
           (ApplyTransformation.txt_of_cic_object 120 GrafiteAst.Declarative "" 
+            ~map_unicode_to_tex:(Helm_registry.get_bool
+              "matita.paste_unicode_as_tex")
             (match 
             (MatitaScript.current ())#grafite_status.GrafiteTypes.proof_status
             with
             | GrafiteTypes.No_proof -> assert false
             | Incomplete_proof i -> 
-                let _,m,p,ty, attrs = i.GrafiteTypes.proof in 
+                let _,m,_subst,p,ty, attrs = i.GrafiteTypes.proof in 
                 Cic.CurrentProof ("current (incomplete) proof",m,p,ty,[],attrs)
-            | Proof (_,m,p,ty, attrs) -> 
+            | Proof (_,m,_subst,p,ty, attrs) -> 
                 Cic.CurrentProof ("current proof",m,p,ty,[],attrs)
             | Intermediate _ -> assert false)));
 (*     addDebugItem "ask record choice"
@@ -248,7 +250,12 @@ let _ =
       List.iter
       (fun (s,t,ul) -> 
           HLog.debug
-           ((String.concat "," (List.map UriManager.name_of_uri ul)) ^ ":"
+           ((String.concat ","
+              (List.map
+                (fun u,saturations ->
+                  UriManager.name_of_uri u ^
+                   "(" ^ string_of_int saturations ^ ")")
+                ul)) ^ ":"
              ^ CoercDb.name_of_carr s ^ " -> " ^ CoercDb.name_of_carr t))
         (CoercDb.to_list ()));
     addDebugSeparator ();