X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_disambiguation%2Fdisambiguate.ml;h=055630971ee5edd3f5ca29b1aea0260c12429c89;hb=cbe0302d6b0d2bca6657fa7479a62d0004665612;hp=0c57754f6f4ddbb85e8c6a8eace5a048eb819c11;hpb=142d3076f2a4dc17d9045c2bba4d4b01eddfd008;p=helm.git

diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml
index 0c57754f6..055630971 100644
--- 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 -> []