diff options
| -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. |