Merge branch 'v8.5'

6 files changed, 69 insertions, 0 deletions

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.
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..4cbae33590
--- /dev/null
+++ b/test-suite/bugs/closed/3510.v
@@ -0,0 +1,5 @@
+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.
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.
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.
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.