diff options
| author | Gaëtan Gilbert | 2019-01-30 14:39:28 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-02-17 15:44:30 +0100 |
| commit | a9f0fd89cf3bb4b728eb451572a96f8599211380 (patch) | |
| tree | 577b7330af67793041cfaba8414005f93fc49c88 /proofs | |
| parent | a49077ef67b8e70696ecacc311fc3070d1b7b461 (diff) | |
Separate variance and universe fields in inductives.
I think the usage looks cleaner this way.
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/proof_global.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 0cfc010c1a..a47fa78f4d 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -268,7 +268,7 @@ let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now let used_univs_body = Vars.universes_of_constr body in let used_univs_typ = Vars.universes_of_constr typ in if allow_deferred then - let initunivs = UState.const_univ_entry ~poly initial_euctx in + let initunivs = UState.univ_entry ~poly initial_euctx in let ctx = constrain_variables universes in (* For vi2vo compilation proofs are computed now but we need to complement the univ constraints of the typ with the ones of @@ -302,7 +302,7 @@ let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now else fun t p -> (* Already checked the univ_decl for the type universes when starting the proof. *) - let univctx = Entries.Monomorphic_const_entry (UState.context_set universes) in + let univctx = UState.univ_entry ~poly:false universes in let t = nf t in Future.from_val (univctx, t), Future.chain p (fun (pt,eff) -> |