aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/bugs')
-rw-r--r--test-suite/bugs/closed/HoTT_coq_056.v4
-rw-r--r--test-suite/bugs/closed/bug_2830.v9
-rw-r--r--test-suite/bugs/closed/bug_3324.v4
-rw-r--r--test-suite/bugs/closed/bug_3454.v6
-rw-r--r--test-suite/bugs/closed/bug_3495.v2
-rw-r--r--test-suite/bugs/closed/bug_3682.v2
-rw-r--r--test-suite/bugs/closed/bug_4498.v2
-rw-r--r--test-suite/bugs/closed/bug_4782.v4
-rw-r--r--test-suite/bugs/closed/bug_4798.v2
-rw-r--r--test-suite/bugs/closed/bug_4836.v2
-rw-r--r--test-suite/bugs/closed/bug_5401.v2
-rw-r--r--test-suite/bugs/closed/bug_7811.v2
-rw-r--r--test-suite/bugs/closed/bug_9166.v2
-rw-r--r--test-suite/bugs/closed/bug_9268.v46
-rw-r--r--test-suite/bugs/closed/bug_9329.v12
-rw-r--r--test-suite/bugs/closed/bug_9375.v16
-rw-r--r--test-suite/bugs/closed/bug_9451.v8
-rw-r--r--test-suite/bugs/closed/bug_9453.v7
-rw-r--r--test-suite/bugs/opened/bug_3890.v2
19 files changed, 116 insertions, 18 deletions
diff --git a/test-suite/bugs/closed/HoTT_coq_056.v b/test-suite/bugs/closed/HoTT_coq_056.v
index 3e3a987a7c..b80e0bb0e4 100644
--- a/test-suite/bugs/closed/HoTT_coq_056.v
+++ b/test-suite/bugs/closed/HoTT_coq_056.v
@@ -94,9 +94,9 @@ Definition FunctorApplicationOf {C D} F {argsT} args {T} {rtn}
Global Arguments FunctorApplicationOf / {C} {D} F {argsT} args {T} {rtn} {_}.
Global Instance FunctorApplicationDash C D (F : Functor C D)
-: FunctorApplicationInterpretable F (IdentityFunctor C) F | 0.
+: FunctorApplicationInterpretable F (IdentityFunctor C) F | 0 := {}.
Global Instance FunctorApplicationFunctorFunctor' A B C C' D (F : Functor (A * B) D) (G : Functor C A) (H : Functor C' B)
-: FunctorApplicationInterpretable F (G, H) (F ∘ (FunctorProduct' G H))%functor | 100.
+: FunctorApplicationInterpretable F (G, H) (F ∘ (FunctorProduct' G H))%functor | 100 := {}.
Notation "F ⟨ x ⟩" := (FunctorApplicationOf F%functor x%functor) : functor_scope.
diff --git a/test-suite/bugs/closed/bug_2830.v b/test-suite/bugs/closed/bug_2830.v
index 801c61b132..a321bb324e 100644
--- a/test-suite/bugs/closed/bug_2830.v
+++ b/test-suite/bugs/closed/bug_2830.v
@@ -194,14 +194,17 @@ Instance skel_equiv A : Equivalence (@skel A).
Admitted.
Import FunctionalExtensionality.
-Instance set_cat : Category Type (fun A B => A -> B) := {
+
+Instance set_cat : Category Type (fun A B => A -> B).
+refine {|
id := fun A => fun x => x
; comp c b a f g := fun x => f (g x)
; eqv := fun A B => @skel (A -> B)
-}.
+|}.
intros. compute. symmetry. apply eta_expansion.
intros. compute. symmetry. apply eta_expansion.
-intros. compute. reflexivity. Defined.
+intros. compute. reflexivity.
+Defined.
(* The [list] type constructor is a Functor. *)
diff --git a/test-suite/bugs/closed/bug_3324.v b/test-suite/bugs/closed/bug_3324.v
index 45dbb57aa2..dae0d4c024 100644
--- a/test-suite/bugs/closed/bug_3324.v
+++ b/test-suite/bugs/closed/bug_3324.v
@@ -6,7 +6,7 @@ Module ETassi.
Record hProp := hp { hproptype :> Type ; isp : IsHProp hproptype}.
Record hSet := BuildhSet {setT:> Type; iss :> IsHSet setT}.
Canonical Structure default_HSet:= fun T P => (@BuildhSet T P).
- Global Instance isset_hProp : IsHSet hProp | 0.
+ Global Instance isset_hProp : IsHSet hProp | 0 := {}.
Check (eq_refl _ : setT (default_HSet _ _) = hProp).
Check (eq_refl _ : setT _ = hProp).
@@ -22,7 +22,7 @@ Module JGross.
Definition Unit_hp:hProp:=(hp Unit admit).
Record hSet := BuildhSet {setT:> Type; iss :> IsHSet setT}.
Canonical Structure default_HSet:= fun T P => (@BuildhSet T P).
- Global Instance isset_hProp : IsHSet hProp | 0.
+ Global Instance isset_hProp : IsHSet hProp | 0 := {}.
Definition isepi {X Y} `(f:X->Y) := forall Z: hSet,
forall g h: Y -> Z, (fun x => g (f x)) = (fun x => h (f x)) -> g = h.
Lemma isepi_issurj {X Y} (f:X->Y): isepi f -> True.
diff --git a/test-suite/bugs/closed/bug_3454.v b/test-suite/bugs/closed/bug_3454.v
index e4cd60cb24..0a01adec33 100644
--- a/test-suite/bugs/closed/bug_3454.v
+++ b/test-suite/bugs/closed/bug_3454.v
@@ -32,14 +32,14 @@ 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)).
+ (@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
: @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 _ _) pr1)) := {}.
(* Toplevel input, characters 221-232: *)
(* Error: *)
(* In environment *)
@@ -52,7 +52,7 @@ 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 _ _)
- (fun s => s.(projT1)))).
+ (fun s => s.(projT1)))) := {}.
(* Toplevel input, characters 15-241:
Error:
Cannot infer an internal placeholder of type "Type" in environment:
diff --git a/test-suite/bugs/closed/bug_3495.v b/test-suite/bugs/closed/bug_3495.v
index 7b0883f910..47db64a096 100644
--- a/test-suite/bugs/closed/bug_3495.v
+++ b/test-suite/bugs/closed/bug_3495.v
@@ -1,7 +1,7 @@
Require Import RelationClasses.
Axiom R : Prop -> Prop -> Prop.
-Declare Instance : Reflexive R.
+Declare Instance R_refl : Reflexive R.
Class bar := { x : False }.
Record foo := { a : Prop ; b : bar }.
diff --git a/test-suite/bugs/closed/bug_3682.v b/test-suite/bugs/closed/bug_3682.v
index 9d37d1a2d0..07b759afb5 100644
--- a/test-suite/bugs/closed/bug_3682.v
+++ b/test-suite/bugs/closed/bug_3682.v
@@ -1,6 +1,6 @@
Require Import TestSuite.admit.
Class Foo.
Definition bar `{Foo} (x : Set) := Set.
-Instance: Foo.
+Instance: Foo := {}.
Definition bar1 := bar nat.
Definition bar2 := bar ltac:(admit).
diff --git a/test-suite/bugs/closed/bug_4498.v b/test-suite/bugs/closed/bug_4498.v
index 379e46b3e3..9b3210860c 100644
--- a/test-suite/bugs/closed/bug_4498.v
+++ b/test-suite/bugs/closed/bug_4498.v
@@ -19,6 +19,6 @@ Class Category := {
Require Export Coq.Setoids.Setoid.
-Add Parametric Morphism `{C : Category} {A B C} : (@compose _ A B C) with
+Add Parametric Morphism `{Category} {A B C} : (@compose _ A B C) with
signature equiv ==> equiv ==> equiv as compose_mor.
Proof. apply comp_respects. Qed.
diff --git a/test-suite/bugs/closed/bug_4782.v b/test-suite/bugs/closed/bug_4782.v
index be17a96f15..c08195d502 100644
--- a/test-suite/bugs/closed/bug_4782.v
+++ b/test-suite/bugs/closed/bug_4782.v
@@ -15,8 +15,8 @@ Record T := { dom : Type }.
Definition pairT A B := {| dom := (dom A * dom B)%type |}.
Class C (A:Type).
Parameter B:T.
-Instance c (A:T) : C (dom A).
-Instance cn : C (dom B).
+Instance c (A:T) : C (dom A) := {}.
+Instance cn : C (dom B) := {}.
Parameter F : forall A:T, C (dom A) -> forall x:dom A, x=x -> A = A.
Set Typeclasses Debug.
Goal forall (A:T) (x:dom A), pairT A A = pairT A A.
diff --git a/test-suite/bugs/closed/bug_4798.v b/test-suite/bugs/closed/bug_4798.v
index 41a1251ca5..696812dee1 100644
--- a/test-suite/bugs/closed/bug_4798.v
+++ b/test-suite/bugs/closed/bug_4798.v
@@ -1,3 +1,5 @@
+(* DO NOT MODIFY THIS FILE DIRECTLY *)
+(* It is autogenerated by dev/tools/update-compat.py. *)
Check match 2 with 0 => 0 | S n => n end.
Notation "|" := 1 (compat "8.7").
Check match 2 with 0 => 0 | S n => n end. (* fails *)
diff --git a/test-suite/bugs/closed/bug_4836.v b/test-suite/bugs/closed/bug_4836.v
index 5838dcd8a7..9aefb10172 100644
--- a/test-suite/bugs/closed/bug_4836.v
+++ b/test-suite/bugs/closed/bug_4836.v
@@ -1 +1 @@
-(* -*- coq-prog-args: ("-compile" "bugs/closed/PLACEHOLDER.v") -*- *)
+(* -*- coq-prog-args: ("bugs/closed/PLACEHOLDER.v") -*- *)
diff --git a/test-suite/bugs/closed/bug_5401.v b/test-suite/bugs/closed/bug_5401.v
index 95193b993b..466e669d00 100644
--- a/test-suite/bugs/closed/bug_5401.v
+++ b/test-suite/bugs/closed/bug_5401.v
@@ -5,7 +5,7 @@ Parameter P : nat -> Type.
Parameter v : forall m, P m.
Parameter f : forall (P : nat -> Type), (forall a, P a) -> P 0.
Class U (R : P 0) (m : forall x, P x) : Prop.
-Instance w : U (f _ (fun _ => v _)) v.
+Instance w : U (f _ (fun _ => v _)) v := {}.
Print HintDb typeclass_instances.
End A.
diff --git a/test-suite/bugs/closed/bug_7811.v b/test-suite/bugs/closed/bug_7811.v
index fee330f22d..155f3285b7 100644
--- a/test-suite/bugs/closed/bug_7811.v
+++ b/test-suite/bugs/closed/bug_7811.v
@@ -1,4 +1,4 @@
-(* -*- mode: coq; coq-prog-args: ("-emacs" "-top" "atomic" "-Q" "." "iris" "-R" "." "stdpp") -*- *)
+(* -*- mode: coq; coq-prog-args: ("-top" "atomic" "-Q" "." "iris" "-R" "." "stdpp") -*- *)
(* File reduced by coq-bug-finder from original input, then from 140 lines to 26 lines, then from 141 lines to 27 lines, then from 142 lines to 27 lines, then from 272 lines to 61 lines, then from 291 lines to 94 lines, then from 678 lines to 142 lines, then from 418 lines to 161 lines, then from 538 lines to 189 lines, then from 840 lines to 493 lines, then from 751 lines to 567 lines, then from 913 lines to 649 lines, then from 875 lines to 666 lines, then from 784 lines to 568 lines, then from 655 lines to 173 lines, then from 317 lines to 94 lines, then from 172 lines to 86 lines, then from 102 lines to 86 lines, then from 130 lines to 86 lines, then from 332 lines to 112 lines, then from 279 lines to 111 lines, then from 3996 lines to 5697 lines, then from 153 lines to 117 lines, then from 146 lines to 108 lines, then from 124 lines to 108 lines *)
(* coqc version 8.8.0 (May 2018) compiled on May 2 2018 16:49:46 with OCaml 4.02.3
coqtop version 8.8.0 (May 2018) *)
diff --git a/test-suite/bugs/closed/bug_9166.v b/test-suite/bugs/closed/bug_9166.v
index 8a7e9c37b0..a89837dd12 100644
--- a/test-suite/bugs/closed/bug_9166.v
+++ b/test-suite/bugs/closed/bug_9166.v
@@ -1,3 +1,5 @@
+(* DO NOT MODIFY THIS FILE DIRECTLY *)
+(* It is autogenerated by dev/tools/update-compat.py. *)
Set Warnings "+deprecated".
Notation bar := option (compat "8.7").
diff --git a/test-suite/bugs/closed/bug_9268.v b/test-suite/bugs/closed/bug_9268.v
new file mode 100644
index 0000000000..02dd46f6d2
--- /dev/null
+++ b/test-suite/bugs/closed/bug_9268.v
@@ -0,0 +1,46 @@
+Require Import Coq.ZArith.ZArith.
+Require Import Coq.micromega.Lia.
+
+Local Open Scope Z_scope.
+
+Definition Register := Z%type.
+
+Definition Opcode := Z%type.
+
+Inductive InstructionI : Type
+ := Lb : Register -> Register -> Z -> InstructionI
+ | InvalidI : InstructionI.
+
+Inductive Instruction : Type
+ := IInstruction : InstructionI -> Instruction.
+
+Definition funct3_LB : Z := 0.
+
+Definition opcode_LOAD : Opcode := 3.
+
+Set Universe Polymorphism.
+
+Definition MachineInt := Z.
+
+Definition funct3_JALR := 0.
+
+Axiom InstructionMapper: Type -> Type.
+
+Definition apply_InstructionMapper(mapper: InstructionMapper Z)(inst: Instruction): Z :=
+ match inst with
+ | IInstruction InvalidI => 2
+ | IInstruction (Lb rd rs1 oimm12) => 3
+ end.
+
+Axiom Encoder: InstructionMapper MachineInt.
+
+Definition encode: Instruction -> MachineInt := apply_InstructionMapper Encoder.
+
+Lemma foo: forall (ins: InstructionI),
+ 0 <= encode (IInstruction ins) ->
+ 0 <= encode (IInstruction ins) .
+Proof.
+ Set Printing Universes.
+ intros.
+ lia.
+Qed.
diff --git a/test-suite/bugs/closed/bug_9329.v b/test-suite/bugs/closed/bug_9329.v
new file mode 100644
index 0000000000..c0322dec40
--- /dev/null
+++ b/test-suite/bugs/closed/bug_9329.v
@@ -0,0 +1,12 @@
+(* Declare empty levels in the same order they are computed *)
+
+Notation "< a ; b ; c >1" :=
+ (sum a (sum b c)) (at level 18, a at level 19, b at level 20, c at level 21).
+Notation "< a ; b ; c >2" :=
+ (sum a (sum b c)) (at level 28, a at level 29, c at level 32, b at level 31).
+Notation "< a ; b ; c >3" :=
+ (sum a (sum b c)) (at level 38, c at level 42, a at level 39, b at level 41).
+Notation "< a ; b ; c >4" :=
+ (sum a (sum b c)) (at level 48, c at level 52, b at level 51, a at level 49).
+Notation "< a ; b >" :=
+ (sum a b) (at level 61, a at level 63, b at level 62).
diff --git a/test-suite/bugs/closed/bug_9375.v b/test-suite/bugs/closed/bug_9375.v
new file mode 100644
index 0000000000..a2bfbafe06
--- /dev/null
+++ b/test-suite/bugs/closed/bug_9375.v
@@ -0,0 +1,16 @@
+Set Primitive Projections.
+
+Record toto : Type := Toto {
+ toto1 : Type;
+ toto2 : toto1 -> Type
+}.
+
+Record tata := Tata {
+ tata1 : Type
+}.
+
+Canonical Structure tata_toto (x : toto) X :=
+ Tata (toto2 x X).
+
+Check fun (T : toto) (t : toto1 T) =>
+ (eq_refl _ : @tata1 _ = @toto2 _ t).
diff --git a/test-suite/bugs/closed/bug_9451.v b/test-suite/bugs/closed/bug_9451.v
new file mode 100644
index 0000000000..03bb0433f1
--- /dev/null
+++ b/test-suite/bugs/closed/bug_9451.v
@@ -0,0 +1,8 @@
+Goal False.
+cut True.
+assert False.
+evar (x : True).
+let v := open_constr:(_) in idtac. all: exfalso; clear.
+Optimize Proof.
+(* Error: Anomaly "grounding a non evar-free term" *)
+Abort All.
diff --git a/test-suite/bugs/closed/bug_9453.v b/test-suite/bugs/closed/bug_9453.v
new file mode 100644
index 0000000000..18745533b2
--- /dev/null
+++ b/test-suite/bugs/closed/bug_9453.v
@@ -0,0 +1,7 @@
+(* check compatibility with 8.8 and earlier for lack of warnings on the nat 5000 *)
+Set Warnings Append "+large-nat,+abstract-large-number".
+Fail Check 5001.
+Check 5000.
+(* Error:
+To avoid stack overflow, large numbers in nat are interpreted as applications of
+Nat.of_uint. *)
diff --git a/test-suite/bugs/opened/bug_3890.v b/test-suite/bugs/opened/bug_3890.v
index 78b2aa69b9..9d83743b2a 100644
--- a/test-suite/bugs/opened/bug_3890.v
+++ b/test-suite/bugs/opened/bug_3890.v
@@ -3,7 +3,9 @@ Set Nested Proofs Allowed.
Class Foo.
Class Bar := b : Type.
+Set Refine Instance Mode.
Instance foo : Foo := _.
+Unset Refine Instance Mode.
(* 1 subgoals, subgoal 1 (ID 4)
============================
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 14:33:04 +0000