diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-07-04 13:38:22 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-07-26 15:11:13 +0200 |
| commit | 4457e6d75affd20c1c13c0d798c490129525bcb5 (patch) | |
| tree | b5eeffe5f1a07c439fe704a6d60b2b036110df7f /proofs | |
| parent | a960c4db9ae93a6445f9db620f96f62b397ba8b5 (diff) | |
More precise type for universe entries.
We use an algebraic type instead of a pair of a boolean and the corresponding
data. For now, this is isomorphic, but this allows later change in the structure.
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/proof_global.ml | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 52d6787d4..2ade797f6 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -378,6 +378,10 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now let t = EConstr.Unsafe.to_constr t in let univstyp, body = make_body t p in let univs, typ = Future.force univstyp in + let univs = + if poly then Entries.Polymorphic_const_entry univs + else Entries.Monomorphic_const_entry univs + in { Entries. const_entry_body = body; const_entry_secctx = section_vars; @@ -386,7 +390,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now const_entry_inline_code = false; const_entry_opaque = true; const_entry_universes = univs; - const_entry_polymorphic = poly}) + }) fpl initial_goals in let binders = Option.map (fun names -> fst (Evd.universe_context ~names (Evd.from_ctx universes))) |