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.
---
 library/declare.mli | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'library/declare.mli')

diff --git a/library/declare.mli b/library/declare.mli
index d8a00db0cf..94cebe3bdc 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -53,9 +53,11 @@ val definition_entry : ?opaque:bool -> ?inline:bool -> ?types:types ->
   constr -> definition_entry
 
 val declare_constant :
+  ?chkguard:bool -> (** default [true] (check guardedness) *)
  ?internal:internal_flag -> ?local:bool -> Id.t -> ?export_seff:bool -> constant_declaration -> constant
 
 val declare_definition : 
+  ?chkguard:bool -> (** default [true] (check guardedness) *)
   ?internal:internal_flag -> ?opaque:bool -> ?kind:definition_object_kind ->
   ?local:bool -> ?poly:polymorphic -> Id.t -> ?types:constr -> 
   constr Univ.in_universe_context_set -> constant
-- 
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
---
 library/declare.mli | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'library/declare.mli')

diff --git a/library/declare.mli b/library/declare.mli
index 94cebe3bdc..cda8855d27 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -53,11 +53,11 @@ val definition_entry : ?opaque:bool -> ?inline:bool -> ?types:types ->
   constr -> definition_entry
 
 val declare_constant :
-  ?chkguard:bool -> (** default [true] (check guardedness) *)
+  ?flags:Declarations.typing_flags -> (** default [check_guarded=true] *)
  ?internal:internal_flag -> ?local:bool -> Id.t -> ?export_seff:bool -> constant_declaration -> constant
 
 val declare_definition : 
-  ?chkguard:bool -> (** default [true] (check guardedness) *)
+  ?flags:Declarations.typing_flags -> (** default [check_guarded=true] *)
   ?internal:internal_flag -> ?opaque:bool -> ?kind:definition_object_kind ->
   ?local:bool -> ?poly:polymorphic -> Id.t -> ?types:constr -> 
   constr Univ.in_universe_context_set -> constant
-- 
cgit v1.2.3