From cb6c3ec2e66e3019cb9ee881b1e222e6e3691463 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 27 Jul 2015 10:50:04 +0200
Subject: Fixing bug #3736 (anomaly instead of error/warning/silence on
 decidability scheme).

Not clear to me why it is not a warning (in verbose mode) rather than
silence when a scheme supposed to be built automatically cannot be
built, as in:

Set Decidable Equality Schemes.
Inductive a := A with b := B.

which could explain why a_beq and a_eq_dec as well as b_beq and
b_eq_dec are not built.
---
 test-suite/bugs/closed/3736.v | 8 ++++++++
 1 file changed, 8 insertions(+)
 create mode 100644 test-suite/bugs/closed/3736.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/3736.v b/test-suite/bugs/closed/3736.v
new file mode 100644
index 0000000000..637b77cc58
--- /dev/null
+++ b/test-suite/bugs/closed/3736.v
@@ -0,0 +1,8 @@
+(* Check non-error failure in case of unsupported decidability scheme *)
+Local Set Decidable Equality Schemes.
+
+Inductive a := A with b := B.
+
+(* But fails with error if explicitly asked for the scheme *)
+
+Fail Scheme Equality for a.
-- 
cgit v1.2.3


From c2a67e6f1cdd803b46a3ff4dc259c1cc57ade33f Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 27 Jul 2015 14:02:50 +0200
Subject: Fixing #4305 (compatibility wrt 8.4 in not interpreting an
 abbreviation not bound to an applied constructor as itself but rather as a
 binding variable as it was the case for non-applied constructor). This was
 broken by e5c02503 while fixed #3483 (Not_found uncaught with a notation to a
 non-constructor).

---
 test-suite/bugs/closed/4305.v | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)
 create mode 100644 test-suite/bugs/closed/4305.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/4305.v b/test-suite/bugs/closed/4305.v
new file mode 100644
index 0000000000..39fc02d22b
--- /dev/null
+++ b/test-suite/bugs/closed/4305.v
@@ -0,0 +1,17 @@
+(* Check fallback when an abbreviation is not interpretable as a pattern *)
+
+Notation foo := Type.
+
+Definition t :=
+  match 0 with
+  | S foo => foo
+  | _ => 0
+  end.
+
+Notation bar := (option Type).
+
+Definition u :=
+  match 0 with
+  | S bar => bar
+  | _ => 0
+  end.
-- 
cgit v1.2.3


From 6d8d39fd0a1c7dac1b6415660fd97fe3ad010ff7 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 27 Jul 2015 18:19:56 +0200
Subject: Test for bug #2243.

---
 test-suite/bugs/closed/2243.v | 9 +++++++++
 1 file changed, 9 insertions(+)
 create mode 100644 test-suite/bugs/closed/2243.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/2243.v b/test-suite/bugs/closed/2243.v
new file mode 100644
index 0000000000..6d45c9a09e
--- /dev/null
+++ b/test-suite/bugs/closed/2243.v
@@ -0,0 +1,9 @@
+Inductive is_nul: nat -> Prop := X: is_nul 0.
+Section O.
+Variable u: nat.
+Variable H: is_nul u.
+Goal True.
+Proof.
+destruct H.
+Undo.
+revert H; intro H; destruct H.
-- 
cgit v1.2.3


From 3bdadb4020c1d3e51957a06c1e3a52744f09148d Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 28 Jul 2015 13:47:39 +0200
Subject: Tests for bugs #3509 and #3510.

---
 test-suite/bugs/closed/3509.v |  6 ++++++
 test-suite/bugs/closed/3510.v | 35 +++++++++++++++++++++++++++++++++++
 test-suite/bugs/opened/3509.v | 19 -------------------
 test-suite/bugs/opened/3510.v | 35 -----------------------------------
 4 files changed, 41 insertions(+), 54 deletions(-)
 create mode 100644 test-suite/bugs/closed/3509.v
 create mode 100644 test-suite/bugs/closed/3510.v
 delete mode 100644 test-suite/bugs/opened/3509.v
 delete mode 100644 test-suite/bugs/opened/3510.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/3509.v b/test-suite/bugs/closed/3509.v
new file mode 100644
index 0000000000..8226622670
--- /dev/null
+++ b/test-suite/bugs/closed/3509.v
@@ -0,0 +1,6 @@
+Inductive T := Foo : T.
+Axiom (b : T) (R : forall x : T, Prop) (f : forall x : T, R x).
+Axiom a1 : match b with Foo => f end = f.
+Axiom a2 : match b with Foo => f b end = f b.
+Hint Rewrite a1 : bar.
+Hint Rewrite a2 : bar.
diff --git a/test-suite/bugs/closed/3510.v b/test-suite/bugs/closed/3510.v
new file mode 100644
index 0000000000..daf265071a
--- /dev/null
+++ b/test-suite/bugs/closed/3510.v
@@ -0,0 +1,35 @@
+Require Import TestSuite.admit.
+Lemma match_option_fn T (b : option T) A B s n
+: match b as b return forall x : A, B b x with
+    | Some k => s k
+    | None => n
+  end
+  = fun x : A => match b as b return B b x with
+                   | Some k => s k x
+                   | None => n x
+                 end.
+admit.
+Defined.
+Lemma match_option_comm_2 T (p : option T) A B R (f : forall (x : A) (y : B x), R x y) (s1 : T -> A) (s2 : forall x : T, B (s1 x)) n1 n2
+: match p as p return R match p with
+                          | Some k => s1 k
+                          | None => n1
+                        end
+                        match p as p return B match p with Some k => s1 k | None => n1 end with
+                          | Some k => s2 k
+                          | None => n2
+                        end with
+    | Some k => f (s1 k) (s2 k)
+    | None => f n1 n2
+  end
+  = f match p return A with
+        | Some k => s1 k
+        | None => n1
+      end
+      match p as p return B match p with Some k => s1 k | None => n1 end with
+        | Some k => s2 k
+        | None => n2
+      end.
+admit.
+Defined.
+Fail Hint Rewrite match_option_fn match_option_comm_2 : matchdb.
diff --git a/test-suite/bugs/opened/3509.v b/test-suite/bugs/opened/3509.v
deleted file mode 100644
index 3913bbb43f..0000000000
--- a/test-suite/bugs/opened/3509.v
+++ /dev/null
@@ -1,19 +0,0 @@
-Require Import TestSuite.admit.
-Lemma match_bool_fn b A B xT xF
-: match b as b return forall x : A, B b x with
-    | true => xT
-    | false => xF
-  end
-  = fun x : A => match b as b return B b x with
-                   | true => xT x
-                   | false => xF x
-                 end.
-admit.
-Defined.
-Lemma match_bool_comm_1 (b : bool) A B (F : forall x : A, B x) t f
-: (if b as b return B (if b then t else f) then F t else F f)
-  = F (if b then t else f).
-admit.
-Defined.
-Hint Rewrite match_bool_fn : matchdb.
-Fail Hint Rewrite match_bool_comm_1 : matchdb.
diff --git a/test-suite/bugs/opened/3510.v b/test-suite/bugs/opened/3510.v
deleted file mode 100644
index daf265071a..0000000000
--- a/test-suite/bugs/opened/3510.v
+++ /dev/null
@@ -1,35 +0,0 @@
-Require Import TestSuite.admit.
-Lemma match_option_fn T (b : option T) A B s n
-: match b as b return forall x : A, B b x with
-    | Some k => s k
-    | None => n
-  end
-  = fun x : A => match b as b return B b x with
-                   | Some k => s k x
-                   | None => n x
-                 end.
-admit.
-Defined.
-Lemma match_option_comm_2 T (p : option T) A B R (f : forall (x : A) (y : B x), R x y) (s1 : T -> A) (s2 : forall x : T, B (s1 x)) n1 n2
-: match p as p return R match p with
-                          | Some k => s1 k
-                          | None => n1
-                        end
-                        match p as p return B match p with Some k => s1 k | None => n1 end with
-                          | Some k => s2 k
-                          | None => n2
-                        end with
-    | Some k => f (s1 k) (s2 k)
-    | None => f n1 n2
-  end
-  = f match p return A with
-        | Some k => s1 k
-        | None => n1
-      end
-      match p as p return B match p with Some k => s1 k | None => n1 end with
-        | Some k => s2 k
-        | None => n2
-      end.
-admit.
-Defined.
-Fail Hint Rewrite match_option_fn match_option_comm_2 : matchdb.
-- 
cgit v1.2.3


From 309907165909a08c4b6c2c05e87f458bb1873f91 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 28 Jul 2015 13:57:00 +0200
Subject: Updating test-suite for #3510.

---
 test-suite/bugs/closed/3510.v | 40 +++++-----------------------------------
 1 file changed, 5 insertions(+), 35 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/3510.v b/test-suite/bugs/closed/3510.v
index daf265071a..4cbae33590 100644
--- a/test-suite/bugs/closed/3510.v
+++ b/test-suite/bugs/closed/3510.v
@@ -1,35 +1,5 @@
-Require Import TestSuite.admit.
-Lemma match_option_fn T (b : option T) A B s n
-: match b as b return forall x : A, B b x with
-    | Some k => s k
-    | None => n
-  end
-  = fun x : A => match b as b return B b x with
-                   | Some k => s k x
-                   | None => n x
-                 end.
-admit.
-Defined.
-Lemma match_option_comm_2 T (p : option T) A B R (f : forall (x : A) (y : B x), R x y) (s1 : T -> A) (s2 : forall x : T, B (s1 x)) n1 n2
-: match p as p return R match p with
-                          | Some k => s1 k
-                          | None => n1
-                        end
-                        match p as p return B match p with Some k => s1 k | None => n1 end with
-                          | Some k => s2 k
-                          | None => n2
-                        end with
-    | Some k => f (s1 k) (s2 k)
-    | None => f n1 n2
-  end
-  = f match p return A with
-        | Some k => s1 k
-        | None => n1
-      end
-      match p as p return B match p with Some k => s1 k | None => n1 end with
-        | Some k => s2 k
-        | None => n2
-      end.
-admit.
-Defined.
-Fail Hint Rewrite match_option_fn match_option_comm_2 : matchdb.
+Inductive T := Foo : T.
+Axiom (b : T) (R : forall x : T, Prop) (f : forall x : T, R x).
+Axiom a1 : match b with Foo => f end = f.
+Axiom a2 : match b with Foo => f b end = f b.
+Hint Rewrite a1 a2 : bar.
-- 
cgit v1.2.3


From 524bff66f40908dc3d17b6a18ee4253a2e61093e Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 28 Jul 2015 17:32:30 +0200
Subject: Adding a test for bug #4280.

---
 test-suite/bugs/closed/4280.v | 24 ++++++++++++++++++++++++
 1 file changed, 24 insertions(+)
 create mode 100644 test-suite/bugs/closed/4280.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/4280.v b/test-suite/bugs/closed/4280.v
new file mode 100644
index 0000000000..fd7897509e
--- /dev/null
+++ b/test-suite/bugs/closed/4280.v
@@ -0,0 +1,24 @@
+Require Import ZArith.
+Require Import Eqdep_dec.
+Local Open Scope Z_scope.
+
+Definition t := { n: Z | n > 1 }.
+
+Program Definition two : t := 2.
+Next Obligation. omega. Qed.
+
+Program Definition t_eq (x y: t) : {x=y} + {x<>y} :=
+  if Z.eq_dec (proj1_sig x) (proj1_sig y) then left _ else right _.
+Next Obligation.
+  destruct x as [x Px], y as [y Py]. simpl in H; subst y.
+  f_equal. apply UIP_dec. decide equality.
+Qed.
+Next Obligation.
+  congruence.
+Qed.
+
+Definition t_list_eq: forall (x y: list t), {x=y} + {x<>y}.
+Proof. decide equality. apply t_eq. Defined.
+
+Goal match t_list_eq (two::nil) (two::nil) with left _ => True | right _ => False end.
+Proof. exact I. Qed.
-- 
cgit v1.2.3