From b1ec686f51c061d47535c408435a47e12a69ac5b Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 20 Dec 2017 18:58:24 +0100 Subject: Force polymorphic definitions to have no internal constraints. The main contender was the abstract tactic that was generating useless constraints for polymorphic subproofs that happened to contain themselves monomorphic subproofs. We had to fix the test-suite for one particular corner-case instance that looked more like a bug than anything else. --- proofs/proof_global.ml | 11 +++++------ 1 file changed, 5 insertions(+), 6 deletions(-) (limited to 'proofs/proof_global.ml') diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 167d6bda0..d04bdb652 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -343,16 +343,15 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now if poly || now then let make_body t (c, eff) = let body = c in - let typ = - if not (keep_body_ucst_separate || not (Safe_typing.empty_private_constants = eff)) then - nf t - else t + let allow_deferred = + not poly && (keep_body_ucst_separate || + not (Safe_typing.empty_private_constants = eff)) in + let typ = if allow_deferred then t else nf t in let env = Global.env () in let used_univs_body = Univops.universes_of_constr env body in let used_univs_typ = Univops.universes_of_constr env typ in - if keep_body_ucst_separate || - not (Safe_typing.empty_private_constants = eff) then + if allow_deferred then let initunivs = UState.const_univ_entry ~poly initial_euctx in let ctx = constrain_variables universes in (* For vi2vo compilation proofs are computed now but we need to -- cgit v1.2.3