From 0b2e68030ec188a4865021bcf2c16f2242289c4b Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Mon, 7 Jan 2019 16:55:38 +0100
Subject: Test for SkySkimmer/coq#13

(NB: this needs relevance mark fixing)
---
 test-suite/bugs/closed/bug_sprop_13.v | 7 +++++++
 1 file changed, 7 insertions(+)
 create mode 100644 test-suite/bugs/closed/bug_sprop_13.v

diff --git a/test-suite/bugs/closed/bug_sprop_13.v b/test-suite/bugs/closed/bug_sprop_13.v
new file mode 100644
index 0000000000..ae80c9c51f
--- /dev/null
+++ b/test-suite/bugs/closed/bug_sprop_13.v
@@ -0,0 +1,7 @@
+(* -*- mode: coq; coq-prog-args: ("-allow-sprop") -*- *)
+Goal forall (P : SProp), P -> P.
+Proof.
+  intros P H. set (H0 := H).
+  (* goal is now H0 *)
+  exact H0.
+Qed.
-- 
cgit v1.2.3