From a585d46fbacfcc9cddf3da439e5f7001d429ba2a Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Tue, 5 Apr 2016 12:56:52 -0400
Subject: Fix bug #4656

I introduced this bug in 4c078b0362542908eb2fe1d63f0d867b339953fd;
Coq.Init.Notations.constructor does not take any arguments.
---
 test-suite/bugs/closed/4656.v | 4 ++++
 1 file changed, 4 insertions(+)
 create mode 100644 test-suite/bugs/closed/4656.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/4656.v b/test-suite/bugs/closed/4656.v
new file mode 100644
index 0000000000..c89a86d634
--- /dev/null
+++ b/test-suite/bugs/closed/4656.v
@@ -0,0 +1,4 @@
+(* -*- coq-prog-args: ("-emacs" "-compat" "8.4") -*- *)
+Goal True.
+  constructor 1.
+Qed.
-- 
cgit v1.2.3


From ab08345ebdb477bf4c83b46e0d8adc29296392f9 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Tue, 5 Apr 2016 13:18:00 -0400
Subject: Add -compat 8.4 econstructor tactics, and tests

Passing `-compat 8.4` now allows the use of `econstructor (tac)`, as in
8.4.
---
 test-suite/success/Compat84.v | 19 +++++++++++++++++++
 1 file changed, 19 insertions(+)
 create mode 100644 test-suite/success/Compat84.v

(limited to 'test-suite')

diff --git a/test-suite/success/Compat84.v b/test-suite/success/Compat84.v
new file mode 100644
index 0000000000..db6348fa17
--- /dev/null
+++ b/test-suite/success/Compat84.v
@@ -0,0 +1,19 @@
+(* -*- coq-prog-args: ("-emacs" "-compat" "8.4") -*- *)
+
+Goal True.
+  solve [ constructor 1 ]. Undo.
+  solve [ econstructor 1 ]. Undo.
+  solve [ constructor ]. Undo.
+  solve [ econstructor ]. Undo.
+  solve [ constructor (fail) ]. Undo.
+  solve [ econstructor (fail) ]. Undo.
+  split.
+Qed.
+
+Goal False \/ True.
+  solve [ constructor (constructor) ]. Undo.
+  solve [ econstructor (econstructor) ]. Undo.
+  solve [ constructor 2; constructor ]. Undo.
+  solve [ econstructor 2; econstructor ]. Undo.
+  right; esplit.
+Qed.
-- 
cgit v1.2.3


From 9f0a896536e709880de5ba638069dea680803f62 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 7 Apr 2016 15:50:26 +0200
Subject: Allow to unset the refinement mode of Instance in ML

Falling back to the global setting if not given.
Useful to make Add Morphism fail correctly when the given proof terms
are incomplete. Adapt test-suite file #2848 accordingly.
---
 test-suite/bugs/closed/2848.v | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/2848.v b/test-suite/bugs/closed/2848.v
index de137d39d1..828e3b8c1f 100644
--- a/test-suite/bugs/closed/2848.v
+++ b/test-suite/bugs/closed/2848.v
@@ -2,8 +2,9 @@ Require Import Setoid.
 
 Parameter value' : Type.
 Parameter equiv' : value' -> value' -> Prop.
-
+Axiom cheat : forall {A}, A.
 Add Parametric Relation : _ equiv'
-  reflexivity proved by (Equivalence.equiv_reflexive _)
-  transitivity proved by (Equivalence.equiv_transitive _)
+  reflexivity proved by (Equivalence.equiv_reflexive cheat)
+  transitivity proved by (Equivalence.equiv_transitive cheat)
     as apply_equiv'_rel.
+Check apply_equiv'_rel : PreOrder equiv'.
\ No newline at end of file
-- 
cgit v1.2.3