diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2016-04-12 18:59:55 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2016-04-12 19:05:30 +0200 |
| commit | 927e88de465e94bf18b970b45faaf97b4c2dff82 (patch) | |
| tree | 9519903aa6cf53dcb1de1958ecaf9b5045469738 /test-suite/bugs | |
| parent | 2bd36760f84f1d79af63cdee4d5d53f289a51204 (diff) | |
Quick fix for #4603 (part 2): Anomaly: Universe undefined
This is a follow-up on Matthieu's 7e7b5684
The Definition command was classified incorrectly when a body was provided.
This fix is a bit ad-hoc. A better one would require more expressiveness in
side effect classification, but I'll do it in trunk only since it could impact
plugins.
Thanks a lot to Enrico for his help!
Diffstat (limited to 'test-suite/bugs')
| -rw-r--r-- | test-suite/bugs/closed/4603.v | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/4603.v b/test-suite/bugs/closed/4603.v new file mode 100644 index 000000000..e7567623a --- /dev/null +++ b/test-suite/bugs/closed/4603.v @@ -0,0 +1,10 @@ +Axiom A : Type. + +Goal True. exact I. +Check (fun P => P A). +Abort. + +Goal True. +Definition foo (A : Type) : Prop:= True. + set (x:=foo). split. +Qed.
\ No newline at end of file |