added annotations to Cic.Implicit

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

diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
index 3959795055c0d8b9a2be4a9009c0f588b4419de5..8403f5f0c082e295da72e48c1764cd27adc24ea2 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
@@ -66,7 +66,7 @@ let debrujin_constructor uri number_of_types =
         C.Var (uri,exp_named_subst')
     | C.Meta _ -> assert false
     | C.Sort _
-    | C.Implicit as t -> t
+    | C.Implicit _ as t -> t
     | C.Cast (te,ty) -> C.Cast (aux k te, aux k ty)
     | 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)
@@ -205,7 +205,7 @@ and does_not_occur context n nn te =
     | C.Rel _
     | C.Meta _
     | C.Sort _
-    | C.Implicit -> true
+    | C.Implicit _ -> true
     | C.Cast (te,ty) ->
        does_not_occur context n nn te && does_not_occur context n nn ty
     | C.Prod (name,so,dest) ->
@@ -567,7 +567,7 @@ and recursive_args context n nn te =
    | C.Var _
    | C.Meta _
    | C.Sort _
-   | C.Implicit
+   | C.Implicit _
    | C.Cast _ (*CSC ??? *) ->
       raise (AssertFailure "3") (* due to type-checking *)
    | C.Prod (name,so,de) ->
@@ -646,7 +646,7 @@ and check_is_really_smaller_arg context n nn kl x safes te =
    | C.Var _
    | C.Meta _
    | C.Sort _
-   | C.Implicit 
+   | C.Implicit _
    | C.Cast _
 (*   | C.Cast (te,ty) ->
       check_is_really_smaller_arg n nn kl x safes te &&
@@ -799,7 +799,7 @@ and guarded_by_destructors context n nn kl x safes =
       )
    | C.Meta _
    | C.Sort _
-   | C.Implicit -> true
+   | C.Implicit _ -> true
    | C.Cast (te,ty) ->
       guarded_by_destructors context n nn kl x safes te &&
        guarded_by_destructors context n nn kl x safes ty
@@ -977,7 +977,7 @@ and guarded_by_constructors context n nn h te args coInductiveTypeURI =
    | C.Rel _ -> true
    | C.Meta _
    | C.Sort _
-   | C.Implicit
+   | C.Implicit _
    | C.Cast _
    | C.Prod _
    | C.LetIn _ ->
@@ -1008,7 +1008,7 @@ and guarded_by_constructors context n nn h te args coInductiveTypeURI =
          | C.Var _
          | C.Sort _ ->
             does_not_occur context n nn te
-         | C.Implicit
+         | C.Implicit _
          | C.Cast _ ->
             raise (AssertFailure "24")(* due to type-checking *)
          | C.Prod (name,so,de) ->
@@ -1042,7 +1042,7 @@ and guarded_by_constructors context n nn h te args coInductiveTypeURI =
          | C.Var _
          | C.Meta _
          | C.Sort _
-         | C.Implicit
+         | C.Implicit _
          | C.Cast _ -> raise (AssertFailure "29")(* due to type-checking *)
          | C.Prod (name,so,de) ->
             begin
@@ -1353,7 +1353,7 @@ and type_of_aux' metasenv context t =
         check_metasenv_consistency metasenv context canonical_context l;
         CicSubstitution.lift_meta l ty
     | C.Sort s -> C.Sort C.Type (*CSC manca la gestione degli universi!!! *)
-    | C.Implicit -> raise (AssertFailure "21")
+    | C.Implicit _ -> raise (AssertFailure "21")
     | C.Cast (te,ty) as t ->
        let _ = type_of_aux context ty in
         if R.are_convertible context (type_of_aux context te) ty then