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

1 files changed, 22 insertions, 25 deletions

diff --git a/test-suite/bugs/closed/3454.v b/test-suite/bugs/closed/3454.v
index c1b6a578f..54f2f83b7 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
+. *)