added annotations to Cic.Implicit

[helm.git] / helm / ocaml / cic_proof_checking / cicSubstitution.ml

diff --git a/helm/ocaml/cic_proof_checking/cicSubstitution.ml b/helm/ocaml/cic_proof_checking/cicSubstitution.ml
index 704a8325ad806803c99f3990726e772fd794b4c5..17ee01b5333c3638e041d5cde49453123e5275c3 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicSubstitution.ml
+++ b/helm/ocaml/cic_proof_checking/cicSubstitution.ml
@@ -54,7 +54,7 @@ let lift n =
        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 (liftaux k te, liftaux k ty)
     | C.Prod (n,s,t) -> C.Prod (n, liftaux k s, liftaux (k+1) t)
     | C.Lambda (n,s,t) -> C.Lambda (n, liftaux k s, liftaux (k+1) t)
@@ -126,7 +126,7 @@ let subst arg =
        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 (substaux k te, substaux k ty)
     | C.Prod (n,s,t) -> C.Prod (n, substaux k s, substaux (k + 1) t)
     | C.Lambda (n,s,t) -> C.Lambda (n, substaux k s, substaux (k + 1) t)
@@ -234,7 +234,7 @@ prerr_endline "---- END\n\n " ;
        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 (substaux k te, substaux k ty)
     | C.Prod (n,s,t) -> C.Prod (n, substaux k s, substaux (k + 1) t)
     | C.Lambda (n,s,t) -> C.Lambda (n, substaux k s, substaux (k + 1) t)
@@ -370,7 +370,7 @@ let lift_meta l t =
        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 (aux k te, aux k ty) (*CSC ??? *)
     | C.Prod (n,s,t) -> C.Prod (n, aux k s, aux (k + 1) t)
     | C.Lambda (n,s,t) -> C.Lambda (n, aux k s, aux (k + 1) t)