]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_transformations/cicAstPp.ml
1. new syntax for patterns:
[helm.git] / helm / ocaml / cic_transformations / cicAstPp.ml
index bb365d73ccf70f14bf38e5c4e166d2bdcfd9396d..8076e006204171a695b0087af9bccc28ebc69757 100644 (file)
@@ -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)
@@ -79,8 +78,7 @@ let rec pp_term = function
   | CicAst.Sort `Type -> "Type"
   | CicAst.Sort `CProp -> "CProp"
   | CicAst.Symbol (name, _) -> name
-
-  | CicAst.UserInput -> ""
+  | 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)