From b46944e7bfedb21734f8dd4c187fae17b606b568 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 26 Dec 2014 10:26:46 +0100 Subject: Call Evd.nf_constraints only on Univ Poly constants When one generates a .vi file only the type is stocked. When one completes a .vi the proof term is stocked but the corresponding type is not changed: - if one minimizes the constraints of the body, the minimization could find that 2 univs are equal and substitute one for the other in the body, but it should also apply the subst to the type orelse coqchk could fail - also, a "retroactive" change of a type (making it stricter) invalidates what was type checked afterwards, so this operation clashes with the vi2vo compilation chain Hence we enable this optimization only for universe polymorphic constants that: - are the ones that truly requires such optimization - are never processed asynchronously, so the scenario above does not apply --- proofs/proof_global.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'proofs') diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 79e86e7a9..d94bc86cd 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -338,7 +338,7 @@ let close_proof ~keep_body_ucst_sepatate ?feedback_id ~now fpl = type closed_proof_output = (Term.constr * Declareops.side_effects) list * Evd.evar_universe_context let return_proof () = - let { proof } = cur_pstate () in + let { proof; strength = (_,poly,_) } = cur_pstate () in let initial_goals = Proof.initial_goals proof in let evd = let error s = raise (Errors.UserError("last tactic before Qed",s)) in @@ -353,7 +353,7 @@ let return_proof () = error(str"Attempt to save a proof with existential " ++ str"variables still non-instantiated") in let eff = Evd.eval_side_effects evd in - let evd = Evd.nf_constraints evd in + let evd = if poly then Evd.nf_constraints evd else evd in (** ppedrot: FIXME, this is surely wrong. There is no reason to duplicate side-effects... This may explain why one need to uniquize side-effects thereafter... *) -- cgit v1.2.3