- Fix the de Bruijn problem in check_projection for good :)

- Fix HoTT coq bug #80, implicit arguments with primitive projections were
wrongly automatically infered.

1 files changed, 4 insertions, 3 deletions

diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index ec9541189a..147fe8a9d2 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -142,9 +142,10 @@ let check_projection env kn inst body =
   let argctx, p = decompose_lam_assum b.(0) in
   (* No need to check the lambdas as the case is well-formed *)
   let () = if not (isRel p) then cannot_recognize () in
-  let arg = destRel p - 1 in
-  let () = if not (arg < Array.length recinfo) then cannot_recognize () in
-  let () = if not (eq_con_chk recinfo.(Array.length recinfo - (arg + 1)) kn) then cannot_recognize () in
+  let var = destRel p in
+  let () = if not (var <= Array.length recinfo) then cannot_recognize () in
+  let arg = Array.length recinfo - var in
+  let () = if not (eq_con_chk recinfo.(arg) kn) then cannot_recognize () in
   let pb = { proj_ind = fst ci.ci_ind;
 	     proj_npars = n;
 	     proj_arg = arg;