added dummy entry in CicAst: UserInput

diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml
index 0c57754f6f4ddbb85e8c6a8eace5a048eb819c11..055630971ee5edd3f5ca29b1aea0260c12429c89 100644 (file)
--- a/helm/ocaml/cic_disambiguation/disambiguate.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguate.ml
@@ -280,6 +280,7 @@ let interpretate ~context ~env ast =
     | CicAst.Sort `CProp -> Cic.Sort Cic.CProp
     | CicAst.Symbol (symbol, instance) ->
         resolve env (Symbol (symbol, instance)) ()
+    | CicAst.UserInput -> assert false
   and aux_option loc context = function
     | None -> Cic.Implicit (Some `Type)
     | Some term -> aux loc context term
@@ -368,6 +369,7 @@ let domain_of_term ~context ast =
           local_context
     | CicAst.Sort _ -> []
     | CicAst.Symbol (symbol, instance) -> [ Symbol (symbol, instance) ]
+    | CicAst.UserInput -> assert false
 
   and aux_option loc context = function
     | None -> []

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

diff --git a/helm/ocaml/cic_transformations/cicAst.ml b/helm/ocaml/cic_transformations/cicAst.ml
index fcc80369794c375c8bbe0b8d825d8cece1f2b701..cb65c2497322e58d98cb12fba14414a2102073f8 100644 (file)
--- a/helm/ocaml/cic_transformations/cicAst.ml
+++ b/helm/ocaml/cic_transformations/cicAst.ml
@@ -75,6 +75,9 @@ type term =
   | Sort of sort_kind
   | Symbol of string * int  (* canonical name, instance *)
 
+  | UserInput (* place holder for user input, used by MatitaConsole, not to be
+              used elsewhere *)
+
 and capture_variable = Cic.name * term option (* name, type *)
 and meta_subst = term option
 and subst = string * term

diff --git a/helm/ocaml/cic_transformations/cicAstPp.ml b/helm/ocaml/cic_transformations/cicAstPp.ml
index dda70793f62c7d3ad9495fed7df032de7b60b185..4c041294990a52d59d588166d559b5ff4a16b6fc 100644 (file)
--- a/helm/ocaml/cic_transformations/cicAstPp.ml
+++ b/helm/ocaml/cic_transformations/cicAstPp.ml
@@ -78,6 +78,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)