X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_disambiguation%2Fdisambiguate.ml;h=b71e908856ba017df051a5d244f7ab39a1fd9035;hb=acf29bdbdcdc6ad8c2d9d27e8a47500981b605cd;hp=4f8f8e78a43a1c9bd34028fc3b5f5b6efe363377;hpb=46f19eadce5f3a11c0ae26934fd8d1b597906416;p=helm.git

diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml
index 4f8f8e78a..b71e90885 100644
--- a/helm/ocaml/cic_disambiguation/disambiguate.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguate.ml
@@ -265,6 +265,8 @@ let interpretate ~context ~env ast =
              CicEnvironment.CircularDependency _ -> 
                raise DisambiguateChoices.Invalid_choice))
     | CicAst.Implicit -> Cic.Implicit None
+    | CicAst.UserInput -> Cic.Implicit (Some `Hole)
+(*    | CicAst.UserInput -> assert false*)
     | CicAst.Num (num, i) -> resolve env (Num i) ~num ()
     | CicAst.Meta (index, subst) ->
         let cic_subst =
@@ -279,7 +281,6 @@ 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