From e8bad8abc7be351a34fdf9770409bbab14bcd6a9 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Fri, 24 Jul 2015 08:46:09 +0200
Subject: Propagate `Guarded` flag from syntax to kernel.

The path is quite a bit of a maze, this commit is not as simple as it ought to be. Something more robust than a boolean should be used here.
---
 kernel/fast_typeops.mli | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'kernel/fast_typeops.mli')

diff --git a/kernel/fast_typeops.mli b/kernel/fast_typeops.mli
index 90d9c55f16..98dbefad13 100644
--- a/kernel/fast_typeops.mli
+++ b/kernel/fast_typeops.mli
@@ -18,6 +18,6 @@ open Environ
  *)
 
 
-val infer      : env -> constr       -> unsafe_judgment
-val infer_v    : env -> constr array -> unsafe_judgment array
-val infer_type : env -> types        -> unsafe_type_judgment
+val infer      : chkguard:bool -> env -> constr       -> unsafe_judgment
+val infer_v    : chkguard:bool -> env -> constr array -> unsafe_judgment array
+val infer_type : chkguard:bool -> env -> types        -> unsafe_type_judgment
-- 
cgit v1.2.3


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/fast_typeops.mli | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

(limited to 'kernel/fast_typeops.mli')

diff --git a/kernel/fast_typeops.mli b/kernel/fast_typeops.mli
index 98dbefad13..1c0146baea 100644
--- a/kernel/fast_typeops.mli
+++ b/kernel/fast_typeops.mli
@@ -8,6 +8,7 @@
 
 open Term
 open Environ
+open Declarations
 
 (** {6 Typing functions (not yet tagged as safe) }
     
@@ -18,6 +19,6 @@ open Environ
  *)
 
 
-val infer      : chkguard:bool -> env -> constr       -> unsafe_judgment
-val infer_v    : chkguard:bool -> env -> constr array -> unsafe_judgment array
-val infer_type : chkguard:bool -> env -> types        -> unsafe_type_judgment
+val infer      : flags:typing_flags -> env -> constr       -> unsafe_judgment
+val infer_v    : flags:typing_flags -> env -> constr array -> unsafe_judgment array
+val infer_type : flags:typing_flags -> env -> types        -> unsafe_type_judgment
-- 
cgit v1.2.3