From 576d7a815174106f337fca2f19ad7f26a7e87cc4 Mon Sep 17 00:00:00 2001 From: Arnaud Spiwack Date: Fri, 26 Jun 2015 11:24:16 +0200 Subject: Add a flag to deactivate guard checking in the kernel. --- kernel/inductive.mli | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) (limited to 'kernel/inductive.mli') diff --git a/kernel/inductive.mli b/kernel/inductive.mli index 5847d25f6..36f32b30c 100644 --- a/kernel/inductive.mli +++ b/kernel/inductive.mli @@ -95,8 +95,11 @@ val inductive_sort_family : one_inductive_body -> sorts_family val check_case_info : env -> pinductive -> case_info -> unit (** {6 Guard conditions for fix and cofix-points. } *) -val check_fix : env -> fixpoint -> unit -val check_cofix : env -> cofixpoint -> unit + +(** When [chk] is false, the guard condition is not actually + checked. *) +val check_fix : env -> chk:bool -> fixpoint -> unit +val check_cofix : env -> chk:bool -> cofixpoint -> unit (** {6 Support for sort-polymorphic inductive types } *) -- cgit v1.2.3