aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/record.ml
diff options
context:
space:
mode:
authorGravatar Matthieu Sozeau <mattam@mattam.org>2017-11-22 18:39:34 +0100
committerGravatar Matthieu Sozeau <mattam@mattam.org>2017-12-01 10:16:49 +0100
commit4fcf1fa32ff395d6bd5f6ce4803eee18173c4d36 (patch)
tree860ae15d5abc8665389d034fd8a1ca80dcd7a353 /vernac/record.ml
parent0d580ce929060df98b7d566a40adc2e46c4a1d6c (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 'vernac/record.ml')
-rw-r--r--vernac/record.ml5
1 files changed, 4 insertions, 1 deletions
diff --git a/vernac/record.ml b/vernac/record.ml
index 1d255b08e..1cdc538b5 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -613,7 +613,7 @@ let definition_structure (kind,cum,poly,finite,(is_coe,((loc,idstruc),pl)),ps,cf
States.with_state_protection (fun () ->
typecheck_params_and_fields finite (kind = Class true) idstruc poly pl s ps notations fs) () in
let sign = structure_signature (fields@params) in
- match kind with
+ let gr = match kind with
| Class def ->
let priorities = List.map (fun id -> {hint_priority = id; hint_pattern = None}) priorities in
let gr = declare_class finite def cum pl univs (loc,idstruc) idbuild
@@ -638,3 +638,6 @@ let definition_structure (kind,cum,poly,finite,(is_coe,((loc,idstruc),pl)),ps,cf
idbuild implpars params arity template implfs
fields is_coe (List.map (fun coe -> not (Option.is_empty coe)) coers) sign in
IndRef ind
+ in
+ Declare.declare_univ_binders gr pl;
+ gr