diff options
author | Matthieu Sozeau <mattam@mattam.org> | 2017-11-22 18:39:34 +0100 |
---|---|---|
committer | Matthieu Sozeau <mattam@mattam.org> | 2017-12-01 10:16:49 +0100 |
commit | 4fcf1fa32ff395d6bd5f6ce4803eee18173c4d36 (patch) | |
tree | 860ae15d5abc8665389d034fd8a1ca80dcd7a353 /proofs/proof_global.ml | |
parent | 0d580ce929060df98b7d566a40adc2e46c4a1d6c (diff) |
Cleanup API for registering universe binders.
- Regularly declared for for polymorphic constants
- Declared globally for monomorphic constants.
E.g mono@{i} := Type@{i} is printed as
mono@{mono.i} := Type@{mono.i}.
There can be a name clash if there's a module and a constant of the
same name. It is detected and is an error if the constant is first
but is not detected and the name for the constant not
registered (??) if the constant comes second.
Accept VarRef when registering universe binders
Fix two problems found by Gaƫtan where binders were not registered properly
Simplify API substantially by not passing around a substructure of an
already carrier-around structure in interpretation/declaration code of
constants and proofs
Fix an issue of the stronger restrict universe context + no evd leak
This is uncovered by not having an evd leak in interp_definition, and
the stronger restrict_universe_context. This patch could be backported
to 8.7, it could also be triggered by the previous restrict_context I
think.
Diffstat (limited to 'proofs/proof_global.ml')
-rw-r--r-- | proofs/proof_global.ml | 8 |
1 files changed, 3 insertions, 5 deletions
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index c1e1c2eda..535ef2013 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -68,17 +68,16 @@ let _ = (* Extra info on proofs. *) type lemma_possible_guards = int list list -type proof_universes = UState.t * Universes.universe_binders option type proof_object = { id : Names.Id.t; entries : Safe_typing.private_constants Entries.definition_entry list; persistence : Decl_kinds.goal_kind; - universes: proof_universes; + universes: UState.t; } type proof_ending = - | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry * proof_universes + | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry * UState.t | Proved of Vernacexpr.opacity_flag * Vernacexpr.lident option * proof_object @@ -333,7 +332,6 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now in let fpl, univs = Future.split2 fpl in let universes = if poly || now then Future.force univs else initial_euctx in - let binders = if poly then Some (UState.universe_binders universes) else None in (* Because of dependent subgoals at the beginning of proofs, we could have existential variables in the initial types of goals, we need to normalise them for the kernel. *) @@ -409,7 +407,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now in let entries = Future.map2 entry_fn fpl initial_goals in { id = pid; entries = entries; persistence = strength; - universes = (universes, binders) }, + universes }, fun pr_ending -> CEphemeron.get terminator pr_ending let return_proof ?(allow_partial=false) () = |