From 4bce91623c2857f843129e927fdadb30a9c87a7e Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 4 Apr 2017 16:33:30 +0200
Subject: Adding tests for chained abstract tactics.

---
 test-suite/success/abstract_chain.v | 43 +++++++++++++++++++++++++++++++++++++
 1 file changed, 43 insertions(+)
 create mode 100644 test-suite/success/abstract_chain.v

(limited to 'test-suite')

diff --git a/test-suite/success/abstract_chain.v b/test-suite/success/abstract_chain.v
new file mode 100644
index 0000000000..0ff61e87f8
--- /dev/null
+++ b/test-suite/success/abstract_chain.v
@@ -0,0 +1,43 @@
+Lemma foo1 : nat -> True.
+Proof.
+intros _.
+assert (H : True -> True).
+{ abstract (exact (fun x => x)) using bar. }
+assert (H' : True).
+{ abstract (exact (bar I)) using qux. }
+exact H'.
+Qed.
+
+Lemma foo2 : True.
+Proof.
+assert (H : True -> True).
+{ abstract (exact (fun x => x)) using bar. }
+assert (H' : True).
+{ abstract (exact (bar I)) using qux. }
+assert (H'' : True).
+{ abstract (exact (bar qux)) using quz. }
+exact H''.
+Qed.
+
+Set Universe Polymorphism.
+
+Lemma foo3 : nat -> True.
+Proof.
+intros _.
+assert (H : True -> True).
+{ abstract (exact (fun x => x)) using bar. }
+assert (H' : True).
+{ abstract (exact (bar I)) using qux. }
+exact H'.
+Qed.
+
+Lemma foo4 : True.
+Proof.
+assert (H : True -> True).
+{ abstract (exact (fun x => x)) using bar. }
+assert (H' : True).
+{ abstract (exact (bar I)) using qux. }
+assert (H'' : True).
+{ abstract (exact (bar qux)) using quz. }
+exact H''.
+Qed.
-- 
cgit v1.2.3