added annotations to Cic.Implicit

[helm.git] / helm / ocaml / cic_unification / cicRefine.ml

diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml
index 77b376d63e1615931f3de6e92d9b93f867f7cc3b..43ecd892915745020599e705acc6c341b583550f 100644 (file)
--- a/helm/ocaml/cic_unification/cicRefine.ml
+++ b/helm/ocaml/cic_unification/cicRefine.ml
@@ -169,7 +169,7 @@ and type_of_aux' metasenv context t =
     | C.Sort s ->
        C.Sort C.Type, (*CSC manca la gestione degli universi!!! *)
         subst,metasenv
-    | C.Implicit -> raise (Impossible 21)
+    | C.Implicit _ -> raise (Impossible 21)
     | C.Cast (te,ty) ->
        let _,subst',metasenv' =
         type_of_aux subst metasenv context ty in