aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/bugs')
-rw-r--r--test-suite/bugs/closed/4708.v8
-rw-r--r--test-suite/bugs/closed/4718.v15
-rw-r--r--test-suite/bugs/closed/4722.v1
l---------test-suite/bugs/closed/4722/tata1
-rw-r--r--test-suite/bugs/closed/4727.v10
-rw-r--r--test-suite/bugs/closed/4745.v35
-rw-r--r--test-suite/bugs/closed/4772.v6
-rw-r--r--test-suite/bugs/opened/4701.v23
-rw-r--r--test-suite/bugs/opened/4717.v19
-rw-r--r--test-suite/bugs/opened/4721.v13
-rw-r--r--test-suite/bugs/opened/4728.v72
-rw-r--r--test-suite/bugs/opened/4755.v34
-rw-r--r--test-suite/bugs/opened/4771.v22
-rw-r--r--test-suite/bugs/opened/4778.v35
-rw-r--r--test-suite/bugs/opened/4781.v94
15 files changed, 388 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/4708.v b/test-suite/bugs/closed/4708.v
new file mode 100644
index 000000000..ad2e58100
--- /dev/null
+++ b/test-suite/bugs/closed/4708.v
@@ -0,0 +1,8 @@
+(*Doc, it hurts when I poke myself.*)
+
+Notation "'" := 1. (* was:
+Setting notation at level 0.
+Toplevel input, characters 0-18:
+> Notation "'" := 1.
+> ^^^^^^^^^^^^^^^^^^
+Anomaly: Uncaught exception Invalid_argument("index out of bounds"). Please report. *)
diff --git a/test-suite/bugs/closed/4718.v b/test-suite/bugs/closed/4718.v
new file mode 100644
index 000000000..12a4e8fc1
--- /dev/null
+++ b/test-suite/bugs/closed/4718.v
@@ -0,0 +1,15 @@
+(*Congruence is weaker than reflexivity when it comes to higher level than necessary equalities:*)
+
+Goal @eq Set nat nat.
+congruence.
+Qed.
+
+Goal @eq Type nat nat.
+congruence. (*bug*)
+Qed.
+
+Variable T : Type.
+
+Goal @eq Type T T.
+congruence.
+Qed.
diff --git a/test-suite/bugs/closed/4722.v b/test-suite/bugs/closed/4722.v
new file mode 100644
index 000000000..f047624c8
--- /dev/null
+++ b/test-suite/bugs/closed/4722.v
@@ -0,0 +1 @@
+(* -*- coq-prog-args: ("-emacs" "-R" "4722" "Foo") -*- *)
diff --git a/test-suite/bugs/closed/4722/tata b/test-suite/bugs/closed/4722/tata
new file mode 120000
index 000000000..b38e66e75
--- /dev/null
+++ b/test-suite/bugs/closed/4722/tata
@@ -0,0 +1 @@
+toto \ No newline at end of file
diff --git a/test-suite/bugs/closed/4727.v b/test-suite/bugs/closed/4727.v
new file mode 100644
index 000000000..3854bbffd
--- /dev/null
+++ b/test-suite/bugs/closed/4727.v
@@ -0,0 +1,10 @@
+(* -*- coq-prog-args: ("-emacs" "-compat" "8.4") -*- *)
+Goal forall (P : Set) (l : P) (P0 : Set) (w w0 : P0) (T : Type) (a : P * T) (o : P -> option P0),
+ (forall (l1 l2 : P) (w1 : P0), o l1 = Some w1 -> o l2 = Some w1 -> l1 = l2) ->
+ o l = Some w -> o (fst a) = Some w0 -> {w = w0} + {w <> w0} -> False.
+Proof.
+ clear; intros ???????? inj H0 H1 H2.
+ destruct H2; intuition subst.
+ eapply inj in H1; [ | eauto ].
+ progress subst. (* should succeed, used to not succeed *)
+Abort.
diff --git a/test-suite/bugs/closed/4745.v b/test-suite/bugs/closed/4745.v
new file mode 100644
index 000000000..c090125e6
--- /dev/null
+++ b/test-suite/bugs/closed/4745.v
@@ -0,0 +1,35 @@
+(*I get an Anomaly in the following code.
+
+```*)
+Require Vector.
+
+Module M.
+ Lemma Vector_map_map :
+ forall A B C (f : A -> B) (g : B -> C) n (v : Vector.t A n),
+ Vector.map g (Vector.map f v) = Vector.map (fun a => g (f a)) v.
+ Proof.
+ induction v; simpl; auto using f_equal.
+ Qed.
+
+ Lemma Vector_map_map_transparent :
+ forall A B C (f : A -> B) (g : B -> C) n (v : Vector.t A n),
+ Vector.map g (Vector.map f v) = Vector.map (fun a => g (f a)) v.
+ Proof.
+ induction v; simpl; auto using f_equal.
+ Defined.
+ (* Anomaly: constant not found in kind_of_head: Coq.Vectors.Vector.t_ind. Please report. *)
+
+ (* strangely, explicitly passing the principle to induction works *)
+ Lemma Vector_map_map_transparent' :
+ forall A B C (f : A -> B) (g : B -> C) n (v : Vector.t A n),
+ Vector.map g (Vector.map f v) = Vector.map (fun a => g (f a)) v.
+ Proof.
+ induction v using Vector.t_ind; simpl; auto using f_equal.
+ Defined.
+End M.
+(*```
+
+Changing any of the following things eliminates the Anomaly
+ * moving the lemma out of the module M to the top level
+ * proving the lemma as a Fixpoint instead of using induction
+ * proving the analogous lemma on lists instead of vectors*)
diff --git a/test-suite/bugs/closed/4772.v b/test-suite/bugs/closed/4772.v
new file mode 100644
index 000000000..c3109fa31
--- /dev/null
+++ b/test-suite/bugs/closed/4772.v
@@ -0,0 +1,6 @@
+
+Record TruncType := BuildTruncType {
+ trunctype_type : Type
+}.
+
+Fail Arguments BuildTruncType _ _ {_}. (* This should fail *)
diff --git a/test-suite/bugs/opened/4701.v b/test-suite/bugs/opened/4701.v
new file mode 100644
index 000000000..9286f0f1f
--- /dev/null
+++ b/test-suite/bugs/opened/4701.v
@@ -0,0 +1,23 @@
+(*Suppose we have*)
+
+ Inductive my_if {A B} : bool -> Type :=
+ | then_case (_ : A) : my_if true
+ | else_case (_ : B) : my_if false.
+ Notation "'If' b 'Then' A 'Else' B" := (@my_if A B b) (at level 10).
+
+(*then here are three inductive type declarations that work:*)
+
+ Inductive I1 :=
+ | i1 (x : I1).
+ Inductive I2 :=
+ | i2 (x : nat).
+ Inductive I3 :=
+ | i3 (b : bool) (x : If b Then I3 Else nat).
+
+(*and here is one that does not, despite being equivalent to [I3]:*)
+
+ Fail Inductive I4 :=
+ | i4 (b : bool) (x : if b then I4 else nat). (* Error: Non strictly positive occurrence of "I4" in
+ "forall b : bool, (if b then I4 else nat) -> I4". *)
+
+(*I think this one should work. I believe this is a conservative extension over CIC: Since [match] statements returning types can always be re-encoded as inductive type families, the analysis should be independent of whether the constructor uses an inductive or a [match] statement.*)
diff --git a/test-suite/bugs/opened/4717.v b/test-suite/bugs/opened/4717.v
new file mode 100644
index 000000000..9ad474672
--- /dev/null
+++ b/test-suite/bugs/opened/4717.v
@@ -0,0 +1,19 @@
+(*See below. They sometimes work, and sometimes do not. Is this a bug?*)
+
+Require Import Omega Psatz.
+
+Definition foo := nat.
+
+Goal forall (n : foo), 0 = n - n.
+Proof. intros. omega. (* works *) Qed.
+
+Goal forall (x n : foo), x = x + n - n.
+Proof.
+ intros.
+ Fail omega. (* Omega can't solve this system *)
+ Fail lia. (* Cannot find witness. *)
+ unfold foo in *.
+ omega. (* works *)
+Qed.
+
+(* Guillaume Melquiond: What matters is the equality. In the first case, it is @eq nat. In the second case, it is @eq foo. The same issue exists for ring and field. So it is not a bug, but it is worth fixing.*)
diff --git a/test-suite/bugs/opened/4721.v b/test-suite/bugs/opened/4721.v
new file mode 100644
index 000000000..1f184b393
--- /dev/null
+++ b/test-suite/bugs/opened/4721.v
@@ -0,0 +1,13 @@
+Variables S1 S2 : Set.
+
+Goal @eq Type S1 S2 -> @eq Type S1 S2.
+intro H.
+Fail tauto.
+assumption.
+Qed.
+
+(*This is in 8.5pl1, and Matthieq Sozeau says: "That's a regression in tauto indeed, which now requires exact equality of the universes, through a non linear goal pattern matching:
+match goal with ?X1 |- ?X1 forces both instances of X1 to be convertible,
+with no additional universe constraints currently, but the two types are
+initially different. This can be fixed easily to allow the same flexibility
+as in 8.4 (or assumption) to unify the universes as well."*)
diff --git a/test-suite/bugs/opened/4728.v b/test-suite/bugs/opened/4728.v
new file mode 100644
index 000000000..230b4beb6
--- /dev/null
+++ b/test-suite/bugs/opened/4728.v
@@ -0,0 +1,72 @@
+(*I'd like the final [Check] in the following to work:*)
+
+Ltac fin_eta_expand :=
+ [ > lazymatch goal with
+ | [ H : _ |- _ ] => clear H
+ end..
+ | lazymatch goal with
+ | [ H : ?T |- ?T ]
+ => exact H
+ | [ |- ?G ]
+ => fail 0 "No hypothesis matching" G
+ end ];
+ let n := numgoals in
+ tryif constr_eq numgoals 0
+ then idtac
+ else fin_eta_expand.
+
+Ltac pre_eta_expand x :=
+ let T := type of x in
+ let G := match goal with |- ?G => G end in
+ unify T G;
+ unshelve econstructor;
+ destruct x;
+ fin_eta_expand.
+
+Ltac eta_expand x :=
+ let v := constr:(ltac:(pre_eta_expand x)) in
+ idtac v;
+ let v := (eval cbv beta iota zeta in v) in
+ exact v.
+
+Notation eta_expand x := (ltac:(eta_expand x)) (only parsing).
+
+Ltac partial_unify eqn :=
+ lazymatch eqn with
+ | ?x = ?x => idtac
+ | ?f ?x = ?g ?y
+ => partial_unify (f = g);
+ (tryif unify x y then
+ idtac
+ else tryif has_evar x then
+ unify x y
+ else tryif has_evar y then
+ unify x y
+ else
+ idtac)
+ | ?x = ?y
+ => idtac;
+ (tryif unify x y then
+ idtac
+ else tryif has_evar x then
+ unify x y
+ else tryif has_evar y then
+ unify x y
+ else
+ idtac)
+ end.
+
+Tactic Notation "{" open_constr(old_record) "with" open_constr(new_record) "}" :=
+ let old_record' := eta_expand old_record in
+ partial_unify (old_record = new_record);
+ eexact new_record.
+
+Set Implicit Arguments.
+Record prod A B := pair { fst : A ; snd : B }.
+Infix "*" := prod : type_scope.
+Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) : core_scope.
+
+Notation "{ old 'with' new }" := (ltac:({ old with new })) (only parsing).
+
+Check ltac:({ (1, 1) with {| snd := 2 |} }).
+Fail Check { (1, 1) with {| snd := 2 |} }. (* Error: Cannot infer this placeholder of type "Type"; should succeed *)
diff --git a/test-suite/bugs/opened/4755.v b/test-suite/bugs/opened/4755.v
new file mode 100644
index 000000000..9cc0d361e
--- /dev/null
+++ b/test-suite/bugs/opened/4755.v
@@ -0,0 +1,34 @@
+(*I'm not sure which behavior is better. But if the change is intentional, it should be documented (I don't think it is), and it'd be nice if there were a flag for this, or if -compat 8.4 restored the old behavior.*)
+
+Require Import Coq.Setoids.Setoid Coq.Classes.Morphisms.
+Definition f (v : option nat) := match v with
+ | Some k => Some k
+ | None => None
+ end.
+
+Axioms F G : (option nat -> option nat) -> Prop.
+Axiom FG : forall f, f None = None -> F f = G f.
+
+Axiom admit : forall {T}, T.
+
+Existing Instance eq_Reflexive.
+
+Global Instance foo (A := nat)
+ : Proper ((pointwise_relation _ eq)
+ ==> eq ==> forall_relation (fun _ => Basics.flip Basics.impl))
+ (@option_rect A (fun _ => Prop)) | 0.
+exact admit.
+Qed.
+
+Global Instance bar (A := nat)
+ : Proper ((pointwise_relation _ eq)
+ ==> eq ==> eq ==> Basics.flip Basics.impl)
+ (@option_rect A (fun _ => Prop)) | 0.
+exact admit.
+Qed.
+
+Goal forall k, option_rect (fun _ => Prop) (fun v : nat => v = v /\ F f) True k.
+Proof.
+ intro.
+ pose proof (_ : (Proper (_ ==> eq ==> _) and)).
+ Fail setoid_rewrite (FG _ _); []. (* In 8.5: Error: Tactic failure: Incorrect number of goals (expected 2 tactics); works in 8.4 *)
diff --git a/test-suite/bugs/opened/4771.v b/test-suite/bugs/opened/4771.v
new file mode 100644
index 000000000..396d74bdb
--- /dev/null
+++ b/test-suite/bugs/opened/4771.v
@@ -0,0 +1,22 @@
+Module Type Foo.
+
+Parameter Inline t : nat.
+
+End Foo.
+
+Module F(X : Foo).
+
+Tactic Notation "foo" ref(x) := idtac.
+
+Ltac g := foo X.t.
+
+End F.
+
+Module N.
+Definition t := 0 + 0.
+End N.
+
+Module K := F(N).
+
+(* Was
+Anomaly: Uncaught exception Not_found. Please report. *)
diff --git a/test-suite/bugs/opened/4778.v b/test-suite/bugs/opened/4778.v
new file mode 100644
index 000000000..633d158e9
--- /dev/null
+++ b/test-suite/bugs/opened/4778.v
@@ -0,0 +1,35 @@
+Require Import Coq.Setoids.Setoid Coq.Classes.Morphisms.
+Definition f (v : option nat) := match v with
+ | Some k => Some k
+ | None => None
+ end.
+
+Axioms F G : (option nat -> option nat) -> Prop.
+Axiom FG : forall f, f None = None -> F f = G f.
+
+Axiom admit : forall {T}, T.
+
+Existing Instance eq_Reflexive.
+
+(* This instance is needed in 8.4, but is useless in 8.5 *)
+Global Instance foo (A := nat)
+ : Proper ((pointwise_relation _ eq)
+ ==> eq ==> forall_relation (fun _ => Basics.flip Basics.impl))
+ (@option_rect A (fun _ => Prop)) | 0.
+exact admit.
+Qed.
+
+(*
+(* This is required in 8.5, but useless in 8.4 *)
+Global Instance bar (A := nat)
+ : Proper ((pointwise_relation _ eq)
+ ==> eq ==> eq ==> Basics.flip Basics.impl)
+ (@option_rect A (fun _ => Prop)) | 0.
+exact admit.
+Qed.
+*)
+
+Goal forall k, option_rect (fun _ => Prop) (fun v : nat => v = v /\ F f) True k. Proof.
+ intro.
+ pose proof (_ : (Proper (_ ==> eq ==> _) and)).
+ Fail setoid_rewrite (FG _ _); [ | reflexivity.. ]. (* this should succeed without [Fail], as it does in 8.4 *)
diff --git a/test-suite/bugs/opened/4781.v b/test-suite/bugs/opened/4781.v
new file mode 100644
index 000000000..8b651ac22
--- /dev/null
+++ b/test-suite/bugs/opened/4781.v
@@ -0,0 +1,94 @@
+Ltac force_clear :=
+ clear;
+ repeat match goal with
+ | [ H : _ |- _ ] => clear H
+ | [ H := _ |- _ ] => clearbody H
+ end.
+
+Class abstract_term {T} (x : T) := by_abstract_term : T.
+Hint Extern 0 (@abstract_term ?T ?x) => force_clear; change T; abstract (exact x) : typeclass_instances.
+
+Goal True.
+(* These work: *)
+ let term := constr:(I) in
+ let T := type of term in
+ let x := constr:((_ : abstract_term term) : T) in
+ pose x.
+ let term := constr:(I) in
+ let T := type of term in
+ let x := constr:((_ : abstract_term term) : T) in
+ let x := (eval cbv iota in (let v : T := x in v)) in
+ pose x.
+ let term := constr:(I) in
+ let T := type of term in
+ let x := constr:((_ : abstract_term term) : T) in
+ let x := match constr:(Set) with ?y => constr:(y) end in
+ pose x.
+(* This fails with an error: *)
+ Fail let term := constr:(I) in
+ let T := type of term in
+ let x := constr:((_ : abstract_term term) : T) in
+ let x := match constr:(x) with ?y => constr:(y) end in
+ pose x. (* The command has indeed failed with message:
+Error: Variable y should be bound to a term. *)
+(* And the rest fail with Anomaly: Uncaught exception Not_found. Please report. *)
+ Fail let term := constr:(I) in
+ let T := type of term in
+ let x := constr:((_ : abstract_term term) : T) in
+ let x := match constr:(x) with ?y => y end in
+ pose x.
+ Fail let term := constr:(I) in
+ let T := type of term in
+ let x := constr:((_ : abstract_term term) : T) in
+ let x := (eval cbv iota in x) in
+ pose x.
+ Fail let term := constr:(I) in
+ let T := type of term in
+ let x := constr:((_ : abstract_term term) : T) in
+ let x := type of x in
+ pose x. (* should succeed *)
+ Fail let term := constr:(I) in
+ let T := type of term in
+ let x := constr:(_ : abstract_term term) in
+ let x := type of x in
+ pose x. (* should succeed *)
+
+(*Apparently what [cbv iota] doesn't see can't hurt it, and [pose] is perfectly happy with abstracted lemmas only some of the time.
+
+Even stranger, consider:*)
+ let term := constr:(I) in
+ let T := type of term in
+ let x := constr:((_ : abstract_term term) : T) in
+ let y := (eval cbv iota in (let v : T := x in v)) in
+ pose y;
+ let x' := fresh "x'" in
+ pose x as x'.
+ let x := (eval cbv delta [x'] in x') in
+ pose x;
+ let z := (eval cbv iota in x) in
+ pose z.
+
+(*This works fine. But if I change the period to a semicolon, I get:*)
+
+ Fail let term := constr:(I) in
+ let T := type of term in
+ let x := constr:((_ : abstract_term term) : T) in
+ let y := (eval cbv iota in (let v : T := x in v)) in
+ pose y;
+ let x' := fresh "x'" in
+ pose x as x';
+ let x := (eval cbv delta [x'] in x') in
+ pose x. (* Anomaly: Uncaught exception Not_found. Please report. *)
+ (* should succeed *)
+(*and if I use the second one instead of [pose x] (note that using [idtac] works fine), I get:*)
+
+ Fail let term := constr:(I) in
+ let T := type of term in
+ let x := constr:((_ : abstract_term term) : T) in
+ let y := (eval cbv iota in (let v : T := x in v)) in
+ pose y;
+ let x' := fresh "x'" in
+ pose x as x';
+ let x := (eval cbv delta [x'] in x') in
+ let z := (eval cbv iota in x) in (* Error: Variable x should be bound to a term. *)
+ idtac. (* should succeed *)