]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_transformations/cicAstPp.ml
added dummy entry in CicAst: UserInput
[helm.git] / helm / ocaml / cic_transformations / cicAstPp.ml
index a854234b78eb1b6be7e40568ec59d86294183ed3..4c041294990a52d59d588166d559b5ff4a16b6fc 100644 (file)
@@ -78,11 +78,13 @@ 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)
 
 and pp_pattern ((head, vars), term) =
-  sprintf "%s -> %s"
+  sprintf "%s \\Rightarrow %s"
     (match vars with
     | [] -> head
     | _ ->