diff options
-rw-r--r-- | test-suite/bugs/closed/3315.v | 1 | ||||
-rw-r--r-- | test-suite/bugs/closed/3317.v | 1 | ||||
-rw-r--r-- | test-suite/bugs/closed/3368.v | 1 | ||||
-rw-r--r-- | test-suite/bugs/closed/3428.v | 1 | ||||
-rw-r--r-- | test-suite/bugs/closed/3454.v | 1 | ||||
-rw-r--r-- | test-suite/bugs/closed/HoTT_coq_089.v | 1 |
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. |