added dummy entry in CicAst: UserInput

[helm.git] / helm / ocaml / cic_transformations / ast2pres.ml

diff --git a/helm/ocaml/cic_transformations/ast2pres.ml b/helm/ocaml/cic_transformations/ast2pres.ml
index cafd80c4a855b70a80b226af93bab225b700b10e..87944aa34f23a98028573c59c3a445fef78ae1c5 100644 (file)
--- a/helm/ocaml/cic_transformations/ast2pres.ml
+++ b/helm/ocaml/cic_transformations/ast2pres.ml
@@ -93,6 +93,8 @@ and countterm current_size t =
     | A.Num (s, _) -> current_size + String.length s
     | A.Sort _ -> current_size + 4 (* sort name *)
     | A.Symbol (s,_) -> current_size + String.length s
+
+    | A.UserInput -> current_size
 ;;
 
 let is_big t = 
@@ -328,6 +330,8 @@ let ast2astBox ?(unicode = true) ?(priority = 0) ?(assoc = false) ?(tail = [])
     | A.Symbol (s, _) -> 
         Box.Text([],s)
 
+    | A.UserInput -> Box.Text([],"")
+
   and aux_option ~tail = function
       None  -> Box.Text([],"_")
     | Some ast -> ast2box ~tail ast 
@@ -463,6 +467,7 @@ let ast2mpres ?(priority = 0) ?(assoc = false) (ast, ids_to_uris) =
     | A.Sort `Type -> P.Mtext ([], "Type")
     | A.Sort `CProp -> P.Mtext ([], "CProp")
     | A.Implicit -> P.Mtext([], "?")
+    | A.UserInput -> P.Mtext([], "")
     | A.Appl [] -> assert false
     | A.Appl ((hd::tl) as l) ->
         let rec find_symbol idref = function