Finish fixes on notations and primitive projections, add test-suite files for closed bugs

4 files changed, 87 insertions, 26 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 5d77c46694..195bd31fe0 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -761,7 +761,8 @@ let intern_qualid loc qid intern env lvar us args =
       let terms = make_subst ids (List.map fst args1) in
       let subst = (terms, Id.Map.empty, Id.Map.empty) in
       let infos = (Id.Map.empty, env) in
-      subst_aconstr_in_glob_constr loc intern lvar subst infos c, false, args2
+      let projapp = match c with NRef _ -> true | _ -> false in
+	subst_aconstr_in_glob_constr loc intern lvar subst infos c, projapp, args2
 
 (* Rule out section vars since these should have been found by intern_var *)
 let intern_non_secvar_qualid loc qid intern env lvar us args =
diff --git a/test-suite/bugs/closed/3428.v b/test-suite/bugs/closed/3428.v
new file mode 100644
index 0000000000..177cdb4f8f
--- /dev/null
+++ b/test-suite/bugs/closed/3428.v
@@ -0,0 +1,34 @@
+(* File reduced by coq-bug-finder from original input, then from 2809 lines to 39 lines *)
+Set Primitive Projections.
+Module Export foo.
+  Record prod (A B : Type) := pair { fst : A ; snd : B }.
+End foo.
+Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a where "x = y" := (@paths _ x y) : type_scope.
+Arguments idpath {A a} , [A] a.
+Definition ap {A B:Type} (f:A -> B) {x y:A} (p:x = y) : f x = f y := match p with idpath => idpath end.
+Axiom path_prod : forall {A B : Type} (z z' : prod A B), (fst z = fst z') -> (snd z = snd z') -> (z = z').
+Notation fst := (@fst _ _).
+Notation snd := (@snd _ _).
+Definition ap_fst_path_prod {A B : Type} {z z' : prod A B} (p : @paths A (fst z) (fst z')) (q : snd z = snd z')
+: ap fst (path_prod z z' p q) = p.
+Abort.
+
+Notation fstp x := (x.(foo.fst)).
+Notation fstap x := (foo.fst x).
+
+Definition ap_fst_path_prod' {A B : Type} {z z' : prod A B} (p : @paths A (fst z) (fst z')) (q : snd z = snd z')
+: ap (fun x => fstap x) (path_prod z z' p q) = p.
+
+Abort.
+
+(* Toplevel input, characters 137-138:
+Error:
+In environment
+A : Type
+B : Type
+z : prod A B
+z' : prod A B
+p : @paths A (foo.fst ?11 ?14 z) (foo.fst ?26 ?29 z')
+q : @paths ?54 (foo.snd ?42 ?45 z) (foo.snd ?57 ?60 z')
+The term "p" has type "@paths A (foo.fst ?11 ?14 z) (foo.fst ?26 ?29 z')"
+while it is expected to have type "@paths A (foo.fst z) (foo.fst z')". *)
\ No newline at end of file
diff --git a/test-suite/bugs/closed/3454.v b/test-suite/bugs/closed/3454.v
index c1b6a578f0..54f2f83b70 100644
--- a/test-suite/bugs/closed/3454.v
+++ b/test-suite/bugs/closed/3454.v
@@ -1,45 +1,41 @@
+Set Primitive Projections.
+Record sigT {A} (P : A -> Type) := existT { projT1 : A ; projT2 : P projT1 }.
+Notation pr1 := (@projT1 _ _).
 
-(* File reduced by coq-bug-finder from original input, then from 5135 lines to 4962 lines, then from 4444 lines to 100 lines, then from 106 lines to 97 lines, then from 105 lines to 28 lines *)
 
-Set Primitive Projections.
+Check (@projT1 _ (fun x : nat => x = x)).
+Check (fun s : @sigT nat (fun x : nat => x = x) => s.(projT1)).
 
-Class Identity {A} (Hom : A -> A -> Type) :=
-  { identity : forall x, Hom x x }.
+Record rimpl {b : bool} {n : nat} := { foo : forall {x : nat}, x = n }. 
 
-Instance eqaid A : Identity (@eq A) :=
-  { identity x := eq_refl }.
+Check (fun r : @rimpl true 0 => r.(foo) (x:=0)).
+Check (fun r : @rimpl true 0 => @foo true 0 r 0).
+Check (fun r : @rimpl true 0 => foo r (x:=0)).
+Check (fun r : @rimpl true 0 => @foo _ _ r 0).
+Check (fun r : @rimpl true 0 => r.(@foo _ _)).
+Check (fun r : @rimpl true 0 => r.(foo)).
 
-Check (identity 0).
+Notation "{ x : T  & P }" := (@sigT T P).
+Notation "{ x : A  & P }" := (sigT (A:=A) (fun x => P)) : type_scope.
+(* Notation "{ x : T * U  & P }" := (@sigT (T * U) P). *)
 
-Record sigT {A} (P : A -> Type) := existT { projT1 : A ; projT2 : P projT1 }.
-Notation pr1 := (@projT1 _ _).
 Definition compose {A B C : Type} (g : B -> C) (f : A -> B) := fun x => g (f x).
 Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a where "x = y" := (@paths _ x y) : type_scope.
 Arguments idpath {A a} , [A] a.
 Class IsEquiv {A B : Type} (f : A -> B) := {}.
 
-
-Notation pr1' x := (x.(projT1)).
-
-
-Notation "{ x : A & P }" := (@sigT A (fun x => P)) : type_scope.
 Local Instance isequiv_tgt_compose A B
 : @IsEquiv (A -> {xy : B * B & fst xy = snd xy})
            (A -> B)
-           (@compose A {xy : B * B & fst xy = snd xy} B (@compose {xy : B * B & fst xy = snd xy} _ B (@snd B B) pr1)).
-
-Local Instance isequiv_tgt_compose' A B
-: @IsEquiv (A -> {xy : B * B & fst xy = snd xy})
-           (A -> B)
-           (@compose A {xy : B * B & fst xy = snd xy} B (@compose {xy : B * B & fst xy = snd xy} _ B (@snd B B) (fun x => pr1' x))).
-
+           (@compose A {xy : B * B & fst xy = snd xy} B
+                     (@compose {xy : B * B & fst xy = snd xy} _ B (@snd B B) pr1)).
 (* Toplevel input, characters 220-223: *)
 (* Error: Cannot infer this placeholder. *)
 
-Local Instance isequiv_tgt_compose''' A B
+Local Instance isequiv_tgt_compose' A B
 : @IsEquiv (A -> {xy : B * B & fst xy = snd xy})
            (A -> B)
-           (@compose A {xy : B * B & fst xy = snd xy} B (@compose {xy : B * B & fst xy = snd xy} _ B (@snd _ _) (@projT1 _ _))).
+           (@compose A {xy : B * B & fst xy = snd xy} B (@compose {xy : B * B & fst xy = snd xy} _ B (@snd _ _) pr1)).
 (* Toplevel input, characters 221-232: *)
 (* Error: *)
 (* In environment *)
@@ -51,7 +47,8 @@ Local Instance isequiv_tgt_compose''' A B
 Local Instance isequiv_tgt_compose'' A B
 : @IsEquiv (A -> {xy : B * B & fst xy = snd xy})
            (A -> B)
-           (@compose A {xy : B * B & fst xy = snd xy} B (@compose {xy : B * B & fst xy = snd xy} _ B (@snd _ _) pr1)).
+           (@compose A {xy : B * B & fst xy = snd xy} B (@compose {xy : B * B & fst xy = snd xy} _ B (@snd _ _) 
+                                                                  (fun s => s.(projT1)))).
 (* Toplevel input, characters 15-241:
 Error:
 Cannot infer an internal placeholder of type "Type" in environment:
@@ -59,4 +56,4 @@ Cannot infer an internal placeholder of type "Type" in environment:
 A : Type
 B : Type
 x : ?32
-. *)
\ No newline at end of file
+. *)
diff --git a/test-suite/bugs/closed/3469.v b/test-suite/bugs/closed/3469.v
new file mode 100644
index 0000000000..bd4f1fcad4
--- /dev/null
+++ b/test-suite/bugs/closed/3469.v
@@ -0,0 +1,29 @@
+(* File reduced by coq-bug-finder from original input, then from 538 lines to 31 lines *)
+Open Scope type_scope.
+Global Set Primitive Projections.
+Set Implicit Arguments.
+Record sig (A : Type) (P : A -> Type) := exist { proj1_sig : A ; proj2_sig : P proj1_sig }.
+Notation sigT := sig (only parsing).
+Notation "{ x : A  & P }" := (sigT (fun x:A => P)) : type_scope.
+Notation projT1 := proj1_sig (only parsing).
+Notation projT2 := proj2_sig (only parsing).
+Variables X : Type.
+Variable R : X -> X -> Type.
+Lemma dependent_choice :
+  (forall x:X, {y : _ & R x y}) ->
+  forall x0, {f : nat -> X & (f O = x0) * (forall n, R (f n) (f (S n)))}.
+Proof.
+  intros H x0.
+  set (f:=fix f n := match n with O => x0 | S n' => projT1 (H (f n')) end).
+  exists f.
+  split.
+  reflexivity.
+  induction n; simpl in *.
+  clear.
+  apply (proj2_sig (H x0)).
+  Undo.
+  apply @proj2_sig. 
+  
+
+(* Toplevel input, characters 21-31:
+Error: Found no subterm matching "proj1_sig ?206" in the current 
\ No newline at end of file