diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-07-03 15:54:02 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-07-03 16:33:27 +0200 |
| commit | e123ec7621d06cde2b65755bab75b438b9f02664 (patch) | |
| tree | 1d114e7e03a8ff283fd7d4021cf0abfe36f22b25 /library/global.mli | |
| parent | 35e0f327405fb659c7ec5f9f7d26ea284aa45810 (diff) | |
Do not add original constraints to the environment in 'with Definition' check.
This was useless, because immediate constraints are assumed to already be in
the current environment, while deferred constraints are useless for the
conversion check of the definition types, as they only appear in the opaque
body.
This also clarifies a bit what is going on in the typing of module constraints
w.r.t. global universes.
Diffstat (limited to 'library/global.mli')
0 files changed, 0 insertions, 0 deletions