added annotations to Cic.Implicit

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

diff --git a/helm/ocaml/cic_unification/cicMetaSubst.ml b/helm/ocaml/cic_unification/cicMetaSubst.ml
index 4ee37168450dc9fc84c409a82a40d9ef25828140..a19bb2b25e405a83b6de8026c0c7b9b2f9795c9d 100644 (file)
--- a/helm/ocaml/cic_unification/cicMetaSubst.ml
+++ b/helm/ocaml/cic_unification/cicMetaSubst.ml
@@ -27,7 +27,7 @@ let apply_subst_gen ~appl_fun subst term =
           in
            C.Meta (i,l'))
     | C.Sort _ as t -> t
-    | C.Implicit -> assert false
+    | C.Implicit _ -> assert false
     | C.Cast (te,ty) -> C.Cast (um_aux te, um_aux ty)
     | C.Prod (n,s,t) -> C.Prod (n, um_aux s, um_aux t)
     | C.Lambda (n,s,t) -> C.Lambda (n, um_aux s, um_aux t)
@@ -280,7 +280,7 @@ let rec force_does_not_occur subst to_be_restricted t =
       C.Rel r when List.mem (r - k) to_be_restricted -> raise Occur
     | C.Rel _
     | C.Sort _ as t -> t
-    | C.Implicit -> assert false
+    | C.Implicit _ -> assert false
     | C.Meta (n, l) ->
        (* we do not retrieve the term associated to ?n in subst since *)
        (* in this way we can restrict if something goes wrong         *)
@@ -516,7 +516,7 @@ let delift n subst context metasenv l t =
            let l' = deliftl 1 l1 in
             C.Meta(i,l')
      | C.Sort _ as t -> t
-     | C.Implicit as t -> t
+     | C.Implicit _ as t -> t
      | C.Cast (te,ty) -> C.Cast (deliftaux k te, deliftaux k ty)
      | C.Prod (n,s,t) -> C.Prod (n, deliftaux k s, deliftaux (k+1) t)
      | C.Lambda (n,s,t) -> C.Lambda (n, deliftaux k s, deliftaux (k+1) t)