X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Facic_content%2FcicNotationPp.ml;h=0d868c0027e1f0e7a53a8755086f213f5ba747ed;hb=3c1a432c1612f8ed21f5b2220005599c4d9da1d5;hp=a994c9fd166b83feb063e6e27a4cca1eed38ebaa;hpb=046ba9f98a41651836720df1e9c2ebb6bd577ea9;p=helm.git

diff --git a/helm/software/components/acic_content/cicNotationPp.ml b/helm/software/components/acic_content/cicNotationPp.ml
index a994c9fd1..0d868c002 100644
--- a/helm/software/components/acic_content/cicNotationPp.ml
+++ b/helm/software/components/acic_content/cicNotationPp.ml
@@ -34,7 +34,7 @@ module Env = CicNotationEnv
    * be added to the output of pp_term.
    * set to false if you need, for example, cut and paste from matitac output to
    * matitatop *)
-let debug_printing = true
+let debug_printing = false
 
 let pp_binder = function
   | `Lambda -> "lambda"
@@ -138,8 +138,8 @@ let rec pp_term ?(pp_parens = true) t =
           (String.concat " and " (List.map map definitions))
           (pp_term term)
     | Ast.Ident (name, Some []) | Ast.Ident (name, None)
-    | Ast.Uri (name, Some []) | Ast.Uri (name, None) ->
-        name
+    | Ast.Uri (name, Some []) | Ast.Uri (name, None) -> name
+    | Ast.NRef nref -> NReference.string_of_reference nref
     | Ast.Ident (name, Some substs)
     | Ast.Uri (name, Some substs) ->
         sprintf "%s \\subst [%s]" name (pp_substs substs)
@@ -147,13 +147,14 @@ let rec pp_term ?(pp_parens = true) t =
     | Ast.Meta (index, substs) ->
         sprintf "%d[%s]" index
           (String.concat "; "
-            (List.map (function None -> "_" | Some t -> pp_term t) substs))
+            (List.map (function None -> "?" | Some t -> pp_term t) substs))
     | Ast.Num (num, _) -> num
     | Ast.Sort `Set -> "Set"
     | Ast.Sort `Prop -> "Prop"
     | Ast.Sort (`Type _) -> "Type"
     | Ast.Sort (`CProp _)-> "CProp"
     | Ast.Sort (`NType s)-> "Type[" ^ s ^ "]"
+    | Ast.Sort (`NCProp s)-> "CProp[" ^ s ^ "]"
     | Ast.Symbol (name, _) -> "'" ^ name
 
     | Ast.UserInput -> ""
@@ -356,8 +357,9 @@ let pp_env env =
 
 let rec pp_cic_appl_pattern = function
   | Ast.UriPattern uri -> UriManager.string_of_uri uri
+  | Ast.NRefPattern nref -> NReference.string_of_reference nref
   | Ast.VarPattern name -> name
-  | Ast.ImplicitPattern -> "_"
+  | Ast.ImplicitPattern -> "?"
   | Ast.ApplPattern aps ->
       sprintf "(%s)" (String.concat " " (List.map pp_cic_appl_pattern aps))