X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Facic_content%2FcicNotationPp.ml;h=0d868c0027e1f0e7a53a8755086f213f5ba747ed;hb=235d5cc96af46d0406bdd28222f56b3ee2bf827e;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..0d868c002 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) @@ -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 ->