added annotations to Cic.Implicit

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

diff --git a/helm/ocaml/cic_proof_checking/cicReductionNaif.ml b/helm/ocaml/cic_proof_checking/cicReductionNaif.ml
index 5dce7c68da4eec64a6b33f09c4cdf365cb99c9e4..4362006447266b1fea7578adca00e4c7e59fa4c4 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicReductionNaif.ml
+++ b/helm/ocaml/cic_proof_checking/cicReductionNaif.ml
@@ -67,7 +67,7 @@ let whd context =
        )
     | C.Meta _ as t -> if l = [] then t else C.Appl (t::l)
     | C.Sort _ as t -> t (* l should be empty *)
-    | C.Implicit as t -> t
+    | C.Implicit _ as t -> t
     | C.Cast (te,ty) -> whdaux l te  (*CSC E' GIUSTO BUTTARE IL CAST? *)
     | C.Prod _ as t -> t (* l should be empty *)
     | C.Lambda (name,s,t) as t' ->
@@ -136,7 +136,7 @@ let whd context =
                 eat_first (r,tl)
               in
                whdaux (ts@l) (List.nth pl (j-1))
-          | C.Cast _ | C.Implicit ->
+          | C.Cast _ | C.Implicit _ ->
              raise (Impossible 2) (* we don't trust our whd ;-) *)
           | _ -> if l = [] then t else C.Appl (t::l)
        )
@@ -290,7 +290,7 @@ let are_convertible =
                 b && aux context ty1 ty2 && aux (tys@context) bo1 bo2)
               fl1 fl2 true
         | (C.Cast _, _) | (_, C.Cast _)
-        | (C.Implicit, _) | (_, C.Implicit) ->
+        | (C.Implicit _, _) | (_, C.Implicit _) ->
            raise (Impossible 3) (* we don't trust our whd ;-) *)
         | (_,_) -> false
     end