moved the expansion of implicits inside the refiner in a lazy way

[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 605b9676e2d5befe11e590de052ed9651d4dac9f..2f7075dacf34fca1004e1a1aeb7d7bcf50c1d851 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
@@ -460,7 +460,8 @@ and are_all_occurrences_positive context uri indparamsno i n nn te =
               C.Rel m when m = n - (indparamsno - k) -> k - 1
             | _ ->
               raise (TypeCheckerFailure
-                (lazy ("Non-positive occurence in mutual inductive definition(s) " ^
+               (lazy 
+               ("Non-positive occurence in mutual inductive definition(s) [1]" ^
                 UriManager.string_of_uri uri)))
         ) indparamsno tl
       in
@@ -468,14 +469,14 @@ and are_all_occurrences_positive context uri indparamsno i n nn te =
         List.fold_right (fun x i -> i && does_not_occur context n nn x) tl true
        else
         raise (TypeCheckerFailure
-          (lazy ("Non-positive occurence in mutual inductive definition(s) " ^
+         (lazy ("Non-positive occurence in mutual inductive definition(s) [2]"^
           UriManager.string_of_uri uri)))
    | C.Rel m when m = i ->
       if indparamsno = 0 then
        true
       else
         raise (TypeCheckerFailure
-          (lazy ("Non-positive occurence in mutual inductive definition(s) " ^
+         (lazy ("Non-positive occurence in mutual inductive definition(s) [3]"^
           UriManager.string_of_uri uri)))
    | C.Prod (C.Anonymous,source,dest) ->
       strictly_positive context n nn source &&