From 8860362de4a26286b0cb20cf4e02edc5209bdbd1 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 1 Oct 2015 23:35:51 +0200 Subject: Univs: Change intf of push_named_def to return the computed universe context Let-bound definitions can be opaque but the whole universe context was not gathered to be discharged at section closing time. --- kernel/safe_typing.mli | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) (limited to 'kernel/safe_typing.mli') diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index b971a1bd4..eac08eb83 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -59,8 +59,11 @@ val is_joined_environment : safe_environment -> bool val push_named_assum : (Id.t * Term.types * bool (* polymorphic *)) Univ.in_universe_context_set -> safe_transformer0 + +(** Returns the full universe context necessary to typecheck the definition + (futures are forced) *) val push_named_def : - Id.t * Entries.definition_entry -> safe_transformer0 + Id.t * Entries.definition_entry -> Univ.universe_context_set safe_transformer (** Insertion of global axioms or definitions *) -- cgit v1.2.3