diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-04-08 11:01:52 +0200 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-04-08 11:14:37 +0200 |
| commit | 9d2b4f62ed6faa01c94945b35087cda47f1b1570 (patch) | |
| tree | dbf6074eaba2c176bec550991a2ca8371a14a15a /library/loadpath.mli | |
| parent | 09b64e4219a5e3d57b6d88990e70a283d36c5662 (diff) | |
Fix universe handling (bug introduced in vi2vo commit)
Inside a section, Let followed by a Proof. Qed. are handled as regular
definitions, hence they have universe constraints coming from the type
and from the body. Only the former set was returned to libstack, but
both sets were added to the global universe graph. Hence, at section
closing time, an incomplete set of universe constraints was added back
to the global graph (End Section replays the libstack) and hence saved
in the .vo file. coqchk was right in reporting missing constraints.
Diffstat (limited to 'library/loadpath.mli')
0 files changed, 0 insertions, 0 deletions