From d4f3a1a807d474050a4e91e16ff7813f1db7f537 Mon Sep 17 00:00:00 2001 From: Arnaud Spiwack Date: Tue, 7 Jun 2016 09:52:43 +0200 Subject: Assume totality: dedicated type rather than bool The rational is that 1. further typing flags may be available in the future 2. it makes it easier to trace and document the argument --- kernel/safe_typing.mli | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'kernel/safe_typing.mli') diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 80b9bb495..c5e43e42a 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -57,16 +57,16 @@ val is_joined_environment : safe_environment -> bool (** Insertion of local declarations (Local or Variables) *) val push_named_assum : - chkguard:bool -> + flags:Declarations.typing_flags -> (Id.t * Term.types) Univ.in_universe_context_set -> safe_transformer0 val push_named_def : - chkguard:bool -> + flags:Declarations.typing_flags -> Id.t * Entries.definition_entry -> safe_transformer0 (** Insertion of global axioms or definitions *) type global_declaration = - | ConstantEntry of Entries.constant_entry * bool (* chkguard *) + | ConstantEntry of Entries.constant_entry * Declarations.typing_flags | GlobalRecipe of Cooking.recipe val add_constant : -- cgit v1.2.3