diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-08-30 18:47:45 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-08-30 19:03:05 +0200 |
| commit | 4582ed1c8f0620941a3c296941b1dc808c95d7fe (patch) | |
| tree | d9d58f831b051fa06c5d014f663299db8f91ae35 /test-suite/bugs | |
| parent | 721637c98514a77d05d080f53f226cab3a8da1e7 (diff) | |
Fix bug #4893: not_evar: unexpected failure in 8.5pl1.
Diffstat (limited to 'test-suite/bugs')
| -rw-r--r-- | test-suite/bugs/closed/4893.v | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/4893.v b/test-suite/bugs/closed/4893.v new file mode 100644 index 000000000..9a35bcf95 --- /dev/null +++ b/test-suite/bugs/closed/4893.v @@ -0,0 +1,4 @@ +Goal True. +evar (P: Prop). +assert (H : P); [|subst P]; [exact I|]. +let T := type of H in not_evar T. |