From f72a67569ec8cb9160d161699302b67919da5686 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 27 Jul 2017 14:54:41 +0200 Subject: Allow declaring universe constraints at definition level. Introduce a "+" modifier for universe and constraint declarations to indicate that these can be extended in the final definition/proof. By default [Definition f] is equivalent to [Definition f@{+|+}], i.e universes can be introduced and constraints as well. For [f@{}] or [f@{i j}], the constraints can be extended, no universe introduced, to maintain compatibility with existing developments. Use [f@{i j | }] to indicate that no constraint (nor universe) can be introduced. These kind of definitions could benefit from asynchronous processing. Declarations of universe binders and constraints also works for monomorphic definitions. --- engine/evd.mli | 4 ++++ 1 file changed, 4 insertions(+) (limited to 'engine/evd.mli') diff --git a/engine/evd.mli b/engine/evd.mli index 3f00a3b0b2..76fa69e313 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -552,6 +552,10 @@ val universe_context : ?names:(Id.t located) list -> evar_map -> val universe_subst : evar_map -> Universes.universe_opt_subst val universes : evar_map -> UGraph.t +type universe_decl = + (Names.Id.t Loc.located list, Univ.Constraint.t) Misctypes.gen_universe_decl + +val check_univ_decl : evar_map -> universe_decl -> Universes.universe_binders * Univ.universe_context val merge_universe_context : evar_map -> evar_universe_context -> evar_map val set_universe_context : evar_map -> evar_universe_context -> evar_map -- cgit v1.2.3 From 8966c9241207b6f5d4ee38508246ee97ed006e72 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Mon, 31 Jul 2017 16:49:06 +0200 Subject: proof_global: cleanup and comment close_proof evd: Move constrain_variables to an operation on UState Necessary to check universe declarations correctly for deferred proofs in particular. --- engine/evd.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'engine/evd.mli') diff --git a/engine/evd.mli b/engine/evd.mli index 76fa69e313..8c3771cd94 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -493,7 +493,7 @@ val empty_evar_universe_context : evar_universe_context val union_evar_universe_context : evar_universe_context -> evar_universe_context -> evar_universe_context val evar_universe_context_subst : evar_universe_context -> Universes.universe_opt_subst -val constrain_variables : Univ.LSet.t -> evar_universe_context -> Univ.constraints +val constrain_variables : Univ.LSet.t -> evar_universe_context -> evar_universe_context val evar_universe_context_of_binders : -- cgit v1.2.3 From cd29948855c2cbd3f4065170e41f8dbe625e1921 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Sat, 9 Sep 2017 14:00:42 +0200 Subject: Don't lose names in UState.universe_context. We dont care about the order of the binder map ([map] in the code) so no need to do tricky things with it. --- engine/evd.mli | 8 +++----- 1 file changed, 3 insertions(+), 5 deletions(-) (limited to 'engine/evd.mli') diff --git a/engine/evd.mli b/engine/evd.mli index 8c3771cd94..abcabe8157 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -547,15 +547,13 @@ val check_leq : evar_map -> Univ.universe -> Univ.universe -> bool val evar_universe_context : evar_map -> evar_universe_context val universe_context_set : evar_map -> Univ.universe_context_set -val universe_context : ?names:(Id.t located) list -> evar_map -> +val universe_context : names:(Id.t located) list -> extensible:bool -> evar_map -> (Id.t * Univ.Level.t) list * Univ.universe_context val universe_subst : evar_map -> Universes.universe_opt_subst val universes : evar_map -> UGraph.t -type universe_decl = - (Names.Id.t Loc.located list, Univ.Constraint.t) Misctypes.gen_universe_decl - -val check_univ_decl : evar_map -> universe_decl -> Universes.universe_binders * Univ.universe_context +val check_univ_decl : evar_map -> UState.universe_decl -> + Universes.universe_binders * Univ.universe_context val merge_universe_context : evar_map -> evar_universe_context -> evar_map val set_universe_context : evar_map -> evar_universe_context -> evar_map -- cgit v1.2.3