diff options
| author | Gaëtan Gilbert | 2019-01-07 16:55:38 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-03-14 15:46:16 +0100 |
| commit | 0b2e68030ec188a4865021bcf2c16f2242289c4b (patch) | |
| tree | 357e69b1974fc4a2fc229373a228fae60a9e5b9f | |
| parent | 06b29ed748a9d9b99c2c08a3788906dbad5417d2 (diff) | |
Test for SkySkimmer/coq#13
(NB: this needs relevance mark fixing)
| -rw-r--r-- | test-suite/bugs/closed/bug_sprop_13.v | 7 |
1 files changed, 7 insertions, 0 deletions
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. |