Fix test-suite files according to new parsing rule for application of primitive

projections.

6 files changed, 6 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/3315.v b/test-suite/bugs/closed/3315.v
index 1aebb5ad2..b69097f92 100644
--- a/test-suite/bugs/closed/3315.v
+++ b/test-suite/bugs/closed/3315.v
@@ -1,5 +1,6 @@
 Set Universe Polymorphism.
 Set Primitive Projections.
+Set Implicit Arguments.
 Record sigT {A : Type} (P : A -> Type) := existT { projT1 : A; projT2 : P projT1 }.
 Arguments existT {A} _ _ _.
 Definition unpack_sigma' {A} {P : A -> Type} (Q : sigT P -> Type) (u : sigT P) :
diff --git a/test-suite/bugs/closed/3317.v b/test-suite/bugs/closed/3317.v
index da3d6818d..8d152894e 100644
--- a/test-suite/bugs/closed/3317.v
+++ b/test-suite/bugs/closed/3317.v
@@ -1,3 +1,4 @@
+Set Implicit Arguments. 
 Module A.
   Set Universe Polymorphism.
   Set Primitive Projections.
diff --git a/test-suite/bugs/closed/3368.v b/test-suite/bugs/closed/3368.v
index 64fb03568..1eff1dba8 100644
--- a/test-suite/bugs/closed/3368.v
+++ b/test-suite/bugs/closed/3368.v
@@ -1,5 +1,6 @@
 (* File reduced by coq-bug-finder from 7411 lines to 2271 lines., then from 889 lines to 119 lines, then from 76 lines to 19 lines *)
 Set Universe Polymorphism.
+Set Implicit Arguments. 
 Set Primitive Projections.
 Record PreCategory := { object :> Type; morphism : object -> object -> Type }.
 Record Functor (C D : PreCategory) :=
diff --git a/test-suite/bugs/closed/3428.v b/test-suite/bugs/closed/3428.v
index 177cdb4f8..3eb75e43a 100644
--- a/test-suite/bugs/closed/3428.v
+++ b/test-suite/bugs/closed/3428.v
@@ -1,5 +1,6 @@
 (* File reduced by coq-bug-finder from original input, then from 2809 lines to 39 lines *)
 Set Primitive Projections.
+Set Implicit Arguments. 
 Module Export foo.
   Record prod (A B : Type) := pair { fst : A ; snd : B }.
 End foo.
diff --git a/test-suite/bugs/closed/3454.v b/test-suite/bugs/closed/3454.v
index 54f2f83b7..ebc79e4f9 100644
--- a/test-suite/bugs/closed/3454.v
+++ b/test-suite/bugs/closed/3454.v
@@ -1,4 +1,5 @@
 Set Primitive Projections.
+Set Implicit Arguments.
 Record sigT {A} (P : A -> Type) := existT { projT1 : A ; projT2 : P projT1 }.
 Notation pr1 := (@projT1 _ _).
 
diff --git a/test-suite/bugs/closed/HoTT_coq_089.v b/test-suite/bugs/closed/HoTT_coq_089.v
index 6841d6b27..2da4aff6a 100644
--- a/test-suite/bugs/closed/HoTT_coq_089.v
+++ b/test-suite/bugs/closed/HoTT_coq_089.v
@@ -1,3 +1,4 @@
+Set Implicit Arguments. 
 Set Universe Polymorphism.
 Set Printing Universes.