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

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

4 files changed, 22 insertions, 14 deletions

diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index ec9541189..147fe8a9d 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;
diff --git a/library/impargs.ml b/library/impargs.ml
index 4fe898994..c7faff33c 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -200,6 +200,9 @@ let add_free_rels_until strict strongly_strict revpat bound env m pos acc =
     | App (f,_) when rig && is_flexible_reference env bound depth f ->
 	if strict then () else
           iter_constr_with_full_binders push_lift (frec false) ed c
+    | Proj (p,c) when rig ->
+      if strict then () else
+        iter_constr_with_full_binders push_lift (frec false) ed c	  
     | Case _ when rig ->
 	if strict then () else
           iter_constr_with_full_binders push_lift (frec false) ed c
diff --git a/pretyping/cases.mli b/pretyping/cases.mli
index 70fa945ff..d875edd79 100644
--- a/pretyping/cases.mli
+++ b/pretyping/cases.mli
@@ -110,3 +110,14 @@ type 'a pattern_matching_problem =
 
 
 val compile : 'a pattern_matching_problem -> Environ.unsafe_judgment
+
+val prepare_predicate :            Loc.t ->
+           (Evarutil.type_constraint ->
+            Environ.env -> Evd.evar_map ref -> 'a -> Environ.unsafe_judgment) ->
+           Evd.evar_map ->
+           Environ.env ->
+           (Term.types * tomatch_type) list ->
+           Context.rel_context list ->
+           Constr.constr option ->
+           'a option -> (Evd.evar_map * Names.name list * Term.constr) list
+
diff --git a/test-suite/bugs/opened/HoTT_coq_080.v b/test-suite/bugs/closed/HoTT_coq_080.v
index 9f6949d39..6b07c3040 100644
--- a/test-suite/bugs/opened/HoTT_coq_080.v
+++ b/test-suite/bugs/closed/HoTT_coq_080.v
@@ -2,7 +2,7 @@ Set Primitive Projections.
 Set Implicit Arguments.
 Set Universe Polymorphism.
 Set Asymmetric Patterns.
-
+Set Printing Projections.
 Inductive sum A B := inl : A -> sum A B | inr : B -> sum A B.
 Inductive Empty :=.
 
@@ -10,7 +10,7 @@ Record category :=
   { ob :> Type;
     hom : ob -> ob -> Type
   }.
-Set Printing All.
+
 Definition sum_category (C D : category) : category :=
   {|
     ob := sum (ob C) (ob D);
@@ -23,12 +23,5 @@ Definition sum_category (C D : category) : category :=
 Goal forall C D (x y : ob (sum_category C D)), Type.
 intros C D x y.
 hnf in x, y.
-Fail exact (hom x y). (* Toplevel input, characters 26-27:
-Error:
-In environment
-C : category
-D : category
-x : sum (ob C) (ob D)
-y : sum (ob C) (ob D)
-The term "x" has type "sum (ob C) (ob D)" while it is expected to have type
- "ob ?16". *)
+exact (hom (sum_category _ _) x y). 
+Defined.
\ No newline at end of file