X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2FcicAstPp.ml;h=bb365d73ccf70f14bf38e5c4e166d2bdcfd9396d;hb=de9a83f286eee12117fb478ea2db18f7faebac9a;hp=dda70793f62c7d3ad9495fed7df032de7b60b185;hpb=9ab5ca8acba80b19a939eea2cd87761507e7128b;p=helm.git

diff --git a/helm/ocaml/cic_transformations/cicAstPp.ml b/helm/ocaml/cic_transformations/cicAstPp.ml
index dda70793f..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
@@ -78,6 +80,8 @@ let rec pp_term = function
   | CicAst.Sort `CProp -> "CProp"
   | CicAst.Symbol (name, _) -> name
 
+  | CicAst.UserInput -> ""
+
 and pp_subst (name, term) = sprintf "%s \\Assign %s" name (pp_term term)
 and pp_substs substs = String.concat "; " (List.map pp_subst substs)