X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2FcicAstPp.ml;h=bb365d73ccf70f14bf38e5c4e166d2bdcfd9396d;hb=de9a83f286eee12117fb478ea2db18f7faebac9a;hp=4c041294990a52d59d588166d559b5ff4a16b6fc;hpb=cbe0302d6b0d2bca6657fa7479a62d0004665612;p=helm.git diff --git a/helm/ocaml/cic_transformations/cicAstPp.ml b/helm/ocaml/cic_transformations/cicAstPp.ml index 4c0412949..bb365d73c 100644 --- a/helm/ocaml/cic_transformations/cicAstPp.ml +++ b/helm/ocaml/cic_transformations/cicAstPp.ml @@ -62,10 +62,12 @@ let rec pp_term = function sprintf "%s = %s" (pp_capture_variable var) (pp_term body)) definitions)) (pp_term term) - | CicAst.Ident (name, Some []) - | CicAst.Ident (name, None) -> + | CicAst.Ident (name, Some []) | CicAst.Ident (name, None) + | CicAst.Uri (name, Some []) | CicAst.Uri (name, None) -> name - | CicAst.Ident (name, Some substs) -> sprintf "%s \\subst [%s]" name (pp_substs substs) + | CicAst.Ident (name, Some substs) + | CicAst.Uri (name, Some substs) -> + sprintf "%s \\subst [%s]" name (pp_substs substs) | CicAst.Implicit -> "?" | CicAst.Meta (index, substs) -> sprintf "%d[%s]" index