]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/acic_content/cicNotationPp.ml
Huge commit with several changes:
[helm.git] / helm / software / components / acic_content / cicNotationPp.ml
index b2cb12f9280120e595e6c90948b5e47b28f75ac3..0d868c0027e1f0e7a53a8755086f213f5ba747ed 100644 (file)
@@ -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)
@@ -357,6 +357,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 ->