Imported Upstream version 8.6upstream/8.6

1 files changed, 25 insertions, 0 deletions

diff --git a/test-suite/success/par_abstract.v b/test-suite/success/par_abstract.v
new file mode 100644
index 00000000..7f6f9d62
--- /dev/null
+++ b/test-suite/success/par_abstract.v
@@ -0,0 +1,25 @@
+Axiom T : Type.
+
+Lemma foo : True * Type.
+Proof.
+  split.
+  par: abstract (exact I || exact T).
+Defined.
+
+(* Yes, these names are generated hence
+   the test is fragile.  I want to assert
+   that abstract was correctly handled
+   by par: *)
+Check foo_subproof.
+Check foo_subproof0.
+Check (refl_equal _ :
+  foo =
+  pair foo_subproof foo_subproof0).
+
+Lemma bar : True * Type.
+Proof.
+  split.
+  par: (exact I || exact T).
+Defined.
+Check (refl_equal _ :
+  bar = pair I T).