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 /kernel | |
| 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 'kernel')
| -rw-r--r-- | kernel/safe_typing.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 8ff01a755..e9be955e8 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -300,7 +300,7 @@ let push_named_def (id,de) senv = let senv = add_constraints (Now cst') senv in let senv' = add_constraints (Now cst) senv in let env'' = safe_push_named (id,Some c,typ) senv'.env in - (cst, {senv' with env=env''}) + (Univ.union_constraints cst cst', {senv' with env=env''}) let push_named_assum (id,t) senv = let (t,cst) = Term_typing.translate_local_assum senv.env t in |