X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=helm%2Focaml%2Fcic_transformations%2FcicAstPp.ml;h=8076e006204171a695b0087af9bccc28ebc69757;hb=12cc5b2b8e7f7bb0b5e315094b008a293a4df6b1;hp=a854234b78eb1b6be7e40568ec59d86294183ed3;hpb=e61bf3a95901c62c7b891fb58b176ac38fb7d8e4;p=helm.git

diff --git a/helm/ocaml/cic_transformations/cicAstPp.ml b/helm/ocaml/cic_transformations/cicAstPp.ml
index a854234b7..8076e0062 100644
--- a/helm/ocaml/cic_transformations/cicAstPp.ml
+++ b/helm/ocaml/cic_transformations/cicAstPp.ml
@@ -35,7 +35,6 @@ let pp_name = function Cic.Anonymous -> "_" | Cic.Name s -> s
 
 let rec pp_term = function
   | CicAst.AttributedTerm (_, term) -> pp_term term
-
   | CicAst.Appl terms ->
       sprintf "(%s)" (String.concat " " (List.map pp_term terms))
   | CicAst.Binder (`Forall, (Cic.Anonymous, typ), body)
@@ -62,10 +61,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
@@ -77,12 +78,13 @@ let rec pp_term = function
   | CicAst.Sort `Type -> "Type"
   | 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)
 
 and pp_pattern ((head, vars), term) =
-  sprintf "%s -> %s"
+  sprintf "%s \\Rightarrow %s"
     (match vars with
     | [] -> head
     | _ ->