diff options
| author | Matthieu Sozeau | 2016-09-28 17:26:14 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2016-09-29 17:49:43 +0200 |
| commit | cf87e73ff4dd0b9c70436d66d326ae839868ba78 (patch) | |
| tree | 1df8eeecc54c7cc1cf30af8a31800e3f694eaad9 /test-suite/bugs | |
| parent | 8e0f29cb69f06b64d74b18b09fb6a717034f1140 (diff) | |
Fix bug #5036 autorewrite, sections and universes
Universe context not properly declared. Improve API
and code in declare.ml to allow declaration of universe contexts,
used by declaration of universes and constraints (separately).
Diffstat (limited to 'test-suite/bugs')
| -rw-r--r-- | test-suite/bugs/closed/5036.v | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/5036.v b/test-suite/bugs/closed/5036.v new file mode 100644 index 0000000000..12c958be67 --- /dev/null +++ b/test-suite/bugs/closed/5036.v @@ -0,0 +1,10 @@ +Section foo. + Context (F : Type -> Type). + Context (admit : forall {T}, F T = True). + Hint Rewrite (fun T => @admit T). + Lemma bad : F False. + Proof. + autorewrite with core. + constructor. + Qed. +End foo. (* Anomaly: Universe Top.16 undefined. Please report. *)
\ No newline at end of file |