X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Facic_content%2FcicNotationPp.ml;h=5eb6b64d2ad26fd1c27a3904bb94126a12176b22;hb=c83721701dbbd44d3d547fdec6c4a5658322f424;hp=b2cb12f9280120e595e6c90948b5e47b28f75ac3;hpb=cfb41205e930ede65c1d19ec7ec6f252e0803d55;p=helm.git

diff --git a/helm/software/components/acic_content/cicNotationPp.ml b/helm/software/components/acic_content/cicNotationPp.ml
index b2cb12f92..5eb6b64d2 100644
--- a/helm/software/components/acic_content/cicNotationPp.ml
+++ b/helm/software/components/acic_content/cicNotationPp.ml
@@ -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)
@@ -294,10 +294,12 @@ let pp_fields pp_term fields =
     (List.map 
       (fun (name,ty,coercion,arity) -> 
         " " ^ name ^ 
-        if coercion then (":" ^ 
-          if arity > 0 then string_of_int arity else "" ^ ">") else ": " ^
-        pp_term ty) fields)
-        
+        (if coercion then 
+	  (":" ^ (if arity > 0 then string_of_int arity else "") ^ "> ") 
+	else ": ") ^
+      pp_term ty)
+    fields)
+
 let pp_obj pp_term = function
  | Ast.Inductive (params, types) ->
     let pp_constructors constructors =
@@ -357,6 +359,7 @@ 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.ApplPattern aps ->