diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-12-20 18:58:24 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-01-11 11:17:34 +0100 |
| commit | b1ec686f51c061d47535c408435a47e12a69ac5b (patch) | |
| tree | 762134a4f927879ecd0ccb70226c683f575a7fe5 /proofs | |
| parent | 15bcba0cb00ef759169d2ef7c3cbc21b57f133d2 (diff) | |
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.
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/proof_global.ml | 11 |
1 files changed, 5 insertions, 6 deletions
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 |