added dummy entry in CicAst: UserInput

[helm.git] / helm / ocaml / cic_disambiguation / disambiguate.ml

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 -> []