From c98ed6692d16784e531f7eb8dbb1460fa20c7766 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 15 May 2017 11:13:31 +0200 Subject: Fix #5255: [Context (x : T := y)] should mean [Let x := y]. --- test-suite/bugs/closed/5255.v | 24 ++++++++++++++++++++++++ 1 file changed, 24 insertions(+) create mode 100644 test-suite/bugs/closed/5255.v (limited to 'test-suite/bugs') diff --git a/test-suite/bugs/closed/5255.v b/test-suite/bugs/closed/5255.v new file mode 100644 index 0000000000..5daaf9edbf --- /dev/null +++ b/test-suite/bugs/closed/5255.v @@ -0,0 +1,24 @@ +Section foo. + Context (x := 1). + Definition foo : x = 1 := eq_refl. +End foo. + +Module Type Foo. + Context (x := 1). + Definition foo : x = 1 := eq_refl. +End Foo. + +Set Universe Polymorphism. + +Inductive unit := tt. +Inductive eq {A} (x y : A) : Type := eq_refl : eq x y. + +Section bar. + Context (x := tt). + Definition bar : eq x tt := eq_refl _ _. +End bar. + +Module Type Bar. + Context (x := tt). + Definition bar : eq x tt := eq_refl _ _. +End Bar. -- cgit v1.2.3 From 6735a7cbcaa3757e4d9ad60cb5a64fb5197b961e Mon Sep 17 00:00:00 2001 From: Paul Steckler Date: Wed, 17 May 2017 11:46:31 -0400 Subject: fix swapping of ids in tuples, bug 5486 --- test-suite/bugs/closed/5486.v | 15 +++++++++++++++ 1 file changed, 15 insertions(+) create mode 100644 test-suite/bugs/closed/5486.v (limited to 'test-suite/bugs') diff --git a/test-suite/bugs/closed/5486.v b/test-suite/bugs/closed/5486.v new file mode 100644 index 0000000000..390133162f --- /dev/null +++ b/test-suite/bugs/closed/5486.v @@ -0,0 +1,15 @@ +Axiom proof_admitted : False. +Tactic Notation "admit" := abstract case proof_admitted. +Goal forall (T : Type) (p : prod (prod T T) bool) (Fm : Set) (f : Fm) (k : + forall _ : T, Fm), + @eq Fm + (k + match p return T with + | pair p0 swap => fst p0 + end) f. + intros. + (* next statement failed in Bug 5486 *) + match goal with + | [ |- ?f (let (a, b) := ?d in @?e a b) = ?rhs ] + => pose (let (a, b) := d in e a b) as t0 + end. -- cgit v1.2.3 From 8c2c92cf47536b93e8e7377e8cfd89342325dbcc Mon Sep 17 00:00:00 2001 From: Paul Steckler Date: Wed, 17 May 2017 12:59:08 -0400 Subject: Fixing bug #5526,allow nonlinear variables in Notation patterns --- test-suite/bugs/closed/5526.v | 3 +++ 1 file changed, 3 insertions(+) create mode 100644 test-suite/bugs/closed/5526.v (limited to 'test-suite/bugs') diff --git a/test-suite/bugs/closed/5526.v b/test-suite/bugs/closed/5526.v new file mode 100644 index 0000000000..88f219be30 --- /dev/null +++ b/test-suite/bugs/closed/5526.v @@ -0,0 +1,3 @@ +Fail Notation "x === x" := (eq_refl x) (at level 10). +Reserved Notation "x === x" (only printing, at level 10). +Notation "x === x" := (eq_refl x) (only printing). -- cgit v1.2.3 From 2125c92aa9d17b27c9a19a59774e7e319e48262b Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Mon, 29 May 2017 18:03:19 +0200 Subject: Omega: use "simpl" only on coefficents, not on atoms (fix #4132) Two issues in one: - some focused_simpl were called on the wrong locations - some focused_simpl were done on whole equations In the two cases, this could be bad if "simpl" goes too far with respect to what omega expects: later calls to "occurrence" might fail. This may happen for instance if an atom isn't a variable, but a let-in (b:=5:Z in the example). --- test-suite/bugs/closed/4132.v | 31 +++++++++++++++++++++++++++++++ 1 file changed, 31 insertions(+) create mode 100644 test-suite/bugs/closed/4132.v (limited to 'test-suite/bugs') diff --git a/test-suite/bugs/closed/4132.v b/test-suite/bugs/closed/4132.v new file mode 100644 index 0000000000..806ffb771f --- /dev/null +++ b/test-suite/bugs/closed/4132.v @@ -0,0 +1,31 @@ + +Require Import ZArith Omega. +Open Scope Z_scope. + +(** bug 4132: omega was using "simpl" either on whole equations, or on + delimited but wrong spots. This was leading to unexpected reductions + when one atom (here [b]) is an evaluable reference instead of a variable. *) + +Lemma foo + (x y x' zxy zxy' z : Z) + (b := 5) + (Ry : - b <= y < b) + (Bx : x' <= b) + (H : - zxy' <= zxy) + (H' : zxy' <= x') : - b <= zxy. +Proof. +omega. (* was: Uncaught exception Invalid_argument("index out of bounds"). *) +Qed. + +Lemma foo2 x y (b := 5) (H1 : x <= y) (H2 : y <= b) : x <= b. +omega. (* Pierre L: according to a comment of bug report #4132, + this might have triggered "index out of bounds" in the past, + but I never managed to reproduce that in any version, + even before my fix. *) +Qed. + +Lemma foo3 x y (b := 0) (H1 : x <= y) (H2 : y <= b) : x <= b. +omega. (* Pierre L: according to a comment of bug report #4132, + this might have triggered "Failure(occurence 2)" in the past, + but I never managed to reproduce that. *) +Qed. -- cgit v1.2.3 From e6c41b96a5ea9f8559acf176cdf997b05ccfb317 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Tue, 30 May 2017 12:10:35 +0200 Subject: Fix bug 5550: "typeclasses eauto with" does not work with section variables. --- test-suite/bugs/closed/5550.v | 10 ++++++++++ 1 file changed, 10 insertions(+) create mode 100644 test-suite/bugs/closed/5550.v (limited to 'test-suite/bugs') diff --git a/test-suite/bugs/closed/5550.v b/test-suite/bugs/closed/5550.v new file mode 100644 index 0000000000..bb1222489a --- /dev/null +++ b/test-suite/bugs/closed/5550.v @@ -0,0 +1,10 @@ +Section foo. + + Variable bar : Prop. + Variable H : bar. + + Goal bar. + typeclasses eauto with foobar. + Qed. + +End foo. -- cgit v1.2.3 From 4af77d01c434ff11f0899d504628f4ff91c49142 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 30 May 2017 12:11:28 -0400 Subject: Add opened bug 5019 --- test-suite/bugs/opened/5019.v | 4 ++++ 1 file changed, 4 insertions(+) create mode 100644 test-suite/bugs/opened/5019.v (limited to 'test-suite/bugs') diff --git a/test-suite/bugs/opened/5019.v b/test-suite/bugs/opened/5019.v new file mode 100644 index 0000000000..09622097c5 --- /dev/null +++ b/test-suite/bugs/opened/5019.v @@ -0,0 +1,4 @@ +Require Import Coq.ZArith.ZArith. +Goal forall (T0 : Z -> Type) (k : nat) d (P : T0 (Z.of_nat (S k)) -> Prop), P d. + clear; intros. + Fail Timeout 1 zify. -- cgit v1.2.3 From 1d6a1036a7c472e1f20c5ec586d2484203a2fe2e Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 30 May 2017 12:48:47 -0400 Subject: Fix bug #5019 (looping zify on dependent types) This fixes [bug #5019](https://coq.inria.fr/bugs/show_bug.cgi?id=5019), "[zify] loops on dependent types"; before, we would see a `Z.of_nat (S ?k)` which could not be turned into `Z.succ (Z.of_nat k)`, add a hypothesis of the shape `0 <= Z.of_nat (S k)`, turn that into a hypothesis of the shape `0 <= Z.succ (Z.of_nat k)`, and loop forever on this. This may not be the "right" fix (there may be cases where `zify` should succeed where it still fails with this change), but this is a pure bugfix in the sense that the only places where it changes the behavior of `zify` are the places where, previously, `zify` looped forever. --- test-suite/bugs/closed/5019.v | 5 +++++ test-suite/bugs/opened/5019.v | 4 ---- 2 files changed, 5 insertions(+), 4 deletions(-) create mode 100644 test-suite/bugs/closed/5019.v delete mode 100644 test-suite/bugs/opened/5019.v (limited to 'test-suite/bugs') diff --git a/test-suite/bugs/closed/5019.v b/test-suite/bugs/closed/5019.v new file mode 100644 index 0000000000..7c973f88b5 --- /dev/null +++ b/test-suite/bugs/closed/5019.v @@ -0,0 +1,5 @@ +Require Import Coq.ZArith.ZArith. +Goal forall (T0 : Z -> Type) (k : nat) d (P : T0 (Z.of_nat (S k)) -> Prop), P d. + clear; intros. + Timeout 1 zify. (* used to loop forever; should take < 0.01 s *) +Admitted. diff --git a/test-suite/bugs/opened/5019.v b/test-suite/bugs/opened/5019.v deleted file mode 100644 index 09622097c5..0000000000 --- a/test-suite/bugs/opened/5019.v +++ /dev/null @@ -1,4 +0,0 @@ -Require Import Coq.ZArith.ZArith. -Goal forall (T0 : Z -> Type) (k : nat) d (P : T0 (Z.of_nat (S k)) -> Prop), P d. - clear; intros. - Fail Timeout 1 zify. -- cgit v1.2.3