From 4fcf1fa32ff395d6bd5f6ce4803eee18173c4d36 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 22 Nov 2017 18:39:34 +0100 Subject: 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. --- vernac/command.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'vernac/command.mli') diff --git a/vernac/command.mli b/vernac/command.mli index 070f3e1120..a1f916c782 100644 --- a/vernac/command.mli +++ b/vernac/command.mli @@ -28,7 +28,7 @@ val do_constraint : polymorphic -> val interp_definition : Vernacexpr.universe_decl_expr option -> local_binder_expr list -> polymorphic -> red_expr option -> constr_expr -> constr_expr option -> Safe_typing.private_constants definition_entry * Evd.evar_map * - Univdecls.universe_decl * Universes.universe_binders * Impargs.manual_implicits + Univdecls.universe_decl * Impargs.manual_implicits val do_definition : Id.t -> definition_kind -> Vernacexpr.universe_decl_expr option -> local_binder_expr list -> red_expr option -> constr_expr -> -- cgit v1.2.3