X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicTypeChecker.ml;h=8403f5f0c082e295da72e48c1764cd27adc24ea2;hb=d3c72d6856cd185e5b3e9f2e8b928b78c7031ed1;hp=b034e3928800e139e80e94e7d2396618f8e66255;hpb=b621ad609dab703c4a8055e2554fe39b1bcfb07c;p=helm.git

diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
index b034e3928..8403f5f0c 100644
--- 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) ->
@@ -631,7 +631,8 @@ and eat_lambdas context n te =
        eat_lambdas ((Some (name,(C.Decl so)))::context) (n - 1) ta
       in
        (te, k + 1, context')
-   | (_, _) -> raise (AssertFailure "9")
+   | (n, te) ->
+       raise (AssertFailure (sprintf "9 (%d, %s)" n (CicPp.ppterm te)))
 
 (*CSC: Tutto quello che segue e' l'intuzione di luca ;-) *)
 and check_is_really_smaller_arg context n nn kl x safes te =
@@ -645,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 &&
@@ -798,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
@@ -976,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 _ ->
@@ -1007,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) ->
@@ -1041,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
@@ -1352,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
@@ -1636,8 +1637,10 @@ in if not res then debug_print ("#### " ^ CicPp.ppterm (type_of_aux context p) ^
         when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) -> (* different from Coq manual!!! *)
          C.Sort s2
     | (C.Sort s1, C.Sort s2) -> C.Sort C.Type (*CSC manca la gestione degli universi!!! *)
-    | (_,_) ->
-      raise (TypeCheckerFailure (sprintf
+    | (C.Meta _, C.Sort _) -> t2'
+    | (C.Meta _, C.Meta (_,[]))
+    | (C.Sort _, C.Meta (_,[])) -> t2'
+    | (_,_) -> raise (TypeCheckerFailure (sprintf
         "Prod: expected two sorts, found = %s, %s" (CicPp.ppterm t1')
           (CicPp.ppterm t2')))