use empty universe in the mono alias phases

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

diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml
index 710efdf021a118aada8820ede5c009b242a11495..7a54049a87a251c4b6f99328f067e4a9698fc8c8 100644 (file)
--- a/helm/matita/matitaMathView.ml
+++ b/helm/matita/matitaMathView.ml
@@ -328,9 +328,9 @@ object (self)
       in
       let _, _, _, annterm = acic_sequent in
       let ast, ids_to_uris =
-        CicNotationRew.ast_of_acic ids_to_inner_sorts annterm
+        TermAcicContent.ast_of_acic ids_to_inner_sorts annterm
       in
-      let pped_ast = CicNotationRew.pp_ast ast in
+      let pped_ast = TermContentPres.pp_ast ast in
       let markup = CicNotationPres.render ids_to_uris pped_ast in
       BoxPp.render_to_string text_width markup
     in
@@ -613,7 +613,7 @@ let blank_uri = BuildTimeConf.blank_uri
 let current_proof_uri = BuildTimeConf.current_proof_uri
 
 type term_source =
-  [ `Ast of DisambiguateTypes.term
+  [ `Ast of CicNotationPt.term
   | `Cic of Cic.term * Cic.metasenv
   | `String of string
   ]
@@ -672,7 +672,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
       f ()
     with exn ->
       if not (Helm_registry.get_bool "matita.debug") then
-        fail (MatitaExcPp.to_string exn)
+        fail (snd (MatitaExcPp.to_string exn))
       else raise exn
   in
   let handle_error' f = (fun () -> handle_error (fun () -> f ())) in