From 9d2b4f62ed6faa01c94945b35087cda47f1b1570 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 8 Apr 2014 11:01:52 +0200 Subject: 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. --- kernel/safe_typing.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'kernel') 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 -- cgit v1.2.3