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