aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--test-suite/bugs/closed/3641.v21
-rw-r--r--test-suite/bugs/closed/3658.v74
-rw-r--r--test-suite/bugs/opened/1773.v10
-rw-r--r--test-suite/bugs/opened/3657.v33
4 files changed, 128 insertions, 10 deletions
diff --git a/test-suite/bugs/closed/3641.v b/test-suite/bugs/closed/3641.v
new file mode 100644
index 0000000000..f47f64ead7
--- /dev/null
+++ b/test-suite/bugs/closed/3641.v
@@ -0,0 +1,21 @@
+(* File reduced by coq-bug-finder from original input, then from 7593 lines to 243 lines, then from 256 lines to 102 lines, then from\
+ 104 lines to 28 lines *)
+(* coqc version trunk (September 2014) compiled on Sep 17 2014 0:22:30 with OCaml 4.01.0
+ coqtop version cagnode16:/afs/csail.mit.edu/u/j/jgross/coq-trunk,trunk (d34e1eed232c84590ddb80d70db9f7f7cf13584a) *)
+Set Implicit Arguments.
+Record prod (A B : Type) := pair { fst : A ; snd : B }.
+Notation "x * y" := (prod x y) : type_scope.
+Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) : core_scope.
+Class UnitSubuniverse := { O : Type -> Type ; O_unit : forall T, T -> O T }.
+Class ReflectiveSubuniverse := { rsubu_usubu : UnitSubuniverse ; O_rectnd : forall {P Q : Type} (f : P -> Q), O P -> Q }.
+Global Existing Instance rsubu_usubu.
+Context {subU : ReflectiveSubuniverse}.
+Goal forall (A B : Type) (x : O A * O B) (x0 : B),
+ { g : _ & O_rectnd (fun z : A * B => (O_unit (fst z), O_unit (snd z)))
+ (O_rectnd (fun a : A => O_unit (a, x0)) (fst x)) =
+ g x0 }.
+ eexists.
+ match goal with
+ | [ |- context[?e] ] => is_evar e; let e' := fresh "e'" in pose (e' := e)
+ end.
+ Fail change ?g with e'. (* Stack overflow *) \ No newline at end of file
diff --git a/test-suite/bugs/closed/3658.v b/test-suite/bugs/closed/3658.v
new file mode 100644
index 0000000000..b1158b9a42
--- /dev/null
+++ b/test-suite/bugs/closed/3658.v
@@ -0,0 +1,74 @@
+(* File reduced by coq-bug-finder from original input, then from 12178 lines to 457 lines, then from 500 lines to 147 lines, then from 175 lines to 56 lines *)
+(* coqc version trunk (September 2014) compiled on Sep 21 2014 16:34:4 with OCaml 4.01.0
+ coqtop version cagnode16:/afs/csail.mit.edu/u/j/jgross/coq-trunk,trunk (eaf864354c3fda9ddc1f03f0b1c7807b6fd44322) *)
+
+Axiom transport : forall {A : Type} (P : A -> Type) {x y : A} (p : x = y) (u : P x), P y.
+Axiom ap : forall {A B:Type} (f:A -> B) {x y:A} (p:x = y), f x = f y.
+Module NonPrim.
+ Class Contr_internal (A : Type) := { center : A ; contr : (forall y : A, center = y) }.
+ Arguments center A {_} / .
+ Inductive trunc_index : Type := minus_two | trunc_S (_ : trunc_index).
+ Notation "-2" := minus_two (at level 0).
+ Fixpoint IsTrunc_internal (n : trunc_index) (A : Type) : Type :=
+ match n with
+ | -2 => Contr_internal A
+ | trunc_S n' => forall (x y : A), IsTrunc_internal n' (x = y)
+ end.
+ Class IsTrunc (n : trunc_index) (A : Type) : Type := Trunc_is_trunc : IsTrunc_internal n A.
+ Notation Contr := (IsTrunc -2).
+ Hint Extern 0 => progress change Contr_internal with Contr in * : typeclass_instances.
+ Goal forall (H : Type) (H0 : H -> H -> Type) (H1 : Type)
+ (H2 : Contr H1) (H3 : H1) (H4 : H1 -> H)
+ (H5 : H0 (H4 (center H1)) (H4 H3))
+ (H6 : H0 (H4 (center H1)) (H4 (center H1))),
+ transport (fun y : H => H0 (H4 (center H1)) y) (ap H4 (contr H3)) H6 = H5.
+ intros.
+ match goal with
+ | [ |- context[contr (center _)] ] => fail 1 "bad"
+ | _ => idtac
+ end.
+ match goal with
+ | [ H : _ |- _ ] => destruct (contr H)
+ end.
+ match goal with
+ | [ |- context[contr (center ?x)] ] => fail 1 "bad" x
+ | _ => idtac
+ end.
+ admit.
+ Defined.
+End NonPrim.
+
+Module Prim.
+ Set Primitive Projections.
+ Class Contr_internal (A : Type) := { center : A ; contr : (forall y : A, center = y) }.
+ Arguments center A {_} / .
+ Inductive trunc_index : Type := minus_two | trunc_S (_ : trunc_index).
+ Notation "-2" := minus_two (at level 0).
+ Fixpoint IsTrunc_internal (n : trunc_index) (A : Type) : Type :=
+ match n with
+ | -2 => Contr_internal A
+ | trunc_S n' => forall (x y : A), IsTrunc_internal n' (x = y)
+ end.
+ Class IsTrunc (n : trunc_index) (A : Type) : Type := Trunc_is_trunc : IsTrunc_internal n A.
+ Notation Contr := (IsTrunc -2).
+ Hint Extern 0 => progress change Contr_internal with Contr in * : typeclass_instances.
+ Goal forall (H : Type) (H0 : H -> H -> Type) (H1 : Type)
+ (H2 : Contr H1) (H3 : H1) (H4 : H1 -> H)
+ (H5 : H0 (H4 (center H1)) (H4 H3))
+ (H6 : H0 (H4 (center H1)) (H4 (center H1))),
+ transport (fun y : H => H0 (H4 (center H1)) y) (ap H4 (contr H3)) H6 = H5.
+ intros.
+ match goal with
+ | [ |- context[contr (center _)] ] => fail 1 "bad"
+ | _ => idtac
+ end.
+ match goal with
+ | [ H : _ |- _ ] => destruct (contr H)
+ end.
+ match goal with
+ | [ |- context[contr (center ?x)] ] => fail 1 "bad" x
+ | _ => idtac
+ end. (* Error: Tactic failure: bad H1. *)
+ admit.
+ Defined.
+End Prim. \ No newline at end of file
diff --git a/test-suite/bugs/opened/1773.v b/test-suite/bugs/opened/1773.v
deleted file mode 100644
index 4aabf19c98..0000000000
--- a/test-suite/bugs/opened/1773.v
+++ /dev/null
@@ -1,10 +0,0 @@
-Goal forall B C : nat -> nat -> Prop, forall k, C 0 k ->
- (exists A, (forall k', C A k' -> B A k') -> B A k).
-Proof.
- intros B C k H.
- econstructor.
- intros X.
- apply X.
- apply H.
-Qed.
-
diff --git a/test-suite/bugs/opened/3657.v b/test-suite/bugs/opened/3657.v
new file mode 100644
index 0000000000..6faec0765e
--- /dev/null
+++ b/test-suite/bugs/opened/3657.v
@@ -0,0 +1,33 @@
+(* Set Primitive Projections. *)
+Class foo {A} {a : A} := { bar := a; baz : bar = bar }.
+Arguments bar {_} _ {_}.
+Instance: forall A a, @foo A a.
+intros; constructor.
+abstract reflexivity.
+Defined.
+Goal @bar _ Set _ = (@bar _ (fun _ : Set => Set) _) nat.
+Proof.
+ Check (bar Set).
+ Check (bar (fun _ : Set => Set)).
+ Fail change (bar (fun _ : Set => Set)) with (bar Set). (* Error: Conversion test raised an anomaly *)
+
+Abort.
+
+
+Module A.
+Universes i j.
+Constraint i < j.
+Variable foo : Type@{i}.
+Goal Type@{i}.
+ Fail let t := constr:(Type@{j}) in
+ change Type with t.
+Abort.
+
+Goal Type@{j}.
+ Fail let t := constr:(Type@{i}) in
+ change Type with t.
+ let t := constr:(Type@{i}) in
+ change t. exact foo.
+Defined.
+
+End A.
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 08:57:36 +0000