]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_transformations/cicAstPp.ml
added syntax for URIs
[helm.git] / helm / ocaml / cic_transformations / cicAstPp.ml
index 4c041294990a52d59d588166d559b5ff4a16b6fc..bb365d73ccf70f14bf38e5c4e166d2bdcfd9396d 100644 (file)
@@ -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