use a dummy location when no location is provided

[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 2ba10d7426926dcb1ccbd095ac3188394e6f4260..b6b40f3d1135727f40b475641861ded329df73f9 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
@@ -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 =
@@ -1348,9 +1349,7 @@ and type_of_aux' metasenv context t =
        decr fdebug ;
        ty
     | C.Meta (n,l) -> 
-       let (_,canonical_context,ty) =
-        List.find (function (m,_,_) -> n = m) metasenv
-       in
+       let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
         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!!! *)
@@ -1638,8 +1637,7 @@ 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
+    | (_,_) -> raise (TypeCheckerFailure (sprintf
         "Prod: expected two sorts, found = %s, %s" (CicPp.ppterm t1')
           (CicPp.ppterm t2')))