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/safe_typing.ml | 13 +++++++------
 1 file changed, 7 insertions(+), 6 deletions(-)

(limited to 'kernel/safe_typing.ml')

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index d9adca0c91..18d8978174 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -332,8 +332,8 @@ let safe_push_named (id,_,_ as d) env =
   Environ.push_named d env
 
 
-let push_named_def (id,de) senv =
-  let c,typ,univs = Term_typing.translate_local_def senv.env id de in
+let push_named_def ~chkguard (id,de) senv =
+  let c,typ,univs = Term_typing.translate_local_def ~chkguard senv.env id de in
   let senv' = push_context univs senv in
   let c, senv' = match c with
     | Def c -> Mod_subst.force_constr c, senv'
@@ -346,9 +346,9 @@ let push_named_def (id,de) senv =
   let env'' = safe_push_named (id,Some c,typ) senv'.env in
     {senv' with env=env''}
 
-let push_named_assum ((id,t),ctx) senv =
+let push_named_assum ~chkguard ((id,t),ctx) senv =
   let senv' = push_context_set ctx senv in
-  let t = Term_typing.translate_local_assum senv'.env t in
+  let t = Term_typing.translate_local_assum ~chkguard senv'.env t in
   let env'' = safe_push_named (id,None,t) senv'.env in
     {senv' with env=env''}
 
@@ -439,13 +439,14 @@ let update_resolver f senv = { senv with modresolver = f senv.modresolver }
 
 (** Insertion of constants and parameters in environment *)
 type global_declaration =
-  | ConstantEntry of Entries.constant_entry
+  | ConstantEntry of Entries.constant_entry * bool (* check guard *)
   | GlobalRecipe of Cooking.recipe
 
 let add_constant dir l decl senv =
   let kn = make_con senv.modpath dir l in
   let cb = match decl with
-    | ConstantEntry ce -> Term_typing.translate_constant senv.env kn ce
+    | ConstantEntry (ce,chkguard) ->
+        Term_typing.translate_constant ~chkguard senv.env kn ce
     | GlobalRecipe r ->
       let cb = Term_typing.translate_recipe senv.env kn r in
       if DirPath.is_empty dir then Declareops.hcons_const_body cb else cb
-- 
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/safe_typing.ml | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

(limited to 'kernel/safe_typing.ml')

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 18d8978174..2cea50d9ec 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -332,8 +332,8 @@ let safe_push_named (id,_,_ as d) env =
   Environ.push_named d env
 
 
-let push_named_def ~chkguard (id,de) senv =
-  let c,typ,univs = Term_typing.translate_local_def ~chkguard senv.env id de in
+let push_named_def ~flags (id,de) senv =
+  let c,typ,univs = Term_typing.translate_local_def ~flags senv.env id de in
   let senv' = push_context univs senv in
   let c, senv' = match c with
     | Def c -> Mod_subst.force_constr c, senv'
@@ -346,9 +346,9 @@ let push_named_def ~chkguard (id,de) senv =
   let env'' = safe_push_named (id,Some c,typ) senv'.env in
     {senv' with env=env''}
 
-let push_named_assum ~chkguard ((id,t),ctx) senv =
+let push_named_assum ~flags ((id,t),ctx) senv =
   let senv' = push_context_set ctx senv in
-  let t = Term_typing.translate_local_assum ~chkguard senv'.env t in
+  let t = Term_typing.translate_local_assum ~flags senv'.env t in
   let env'' = safe_push_named (id,None,t) senv'.env in
     {senv' with env=env''}
 
@@ -439,14 +439,14 @@ let update_resolver f senv = { senv with modresolver = f senv.modresolver }
 
 (** Insertion of constants and parameters in environment *)
 type global_declaration =
-  | ConstantEntry of Entries.constant_entry * bool (* check guard *)
+  | ConstantEntry of Entries.constant_entry * Declarations.typing_flags
   | GlobalRecipe of Cooking.recipe
 
 let add_constant dir l decl senv =
   let kn = make_con senv.modpath dir l in
   let cb = match decl with
-    | ConstantEntry (ce,chkguard) ->
-        Term_typing.translate_constant ~chkguard senv.env kn ce
+    | ConstantEntry (ce,flags) ->
+        Term_typing.translate_constant ~flags senv.env kn ce
     | GlobalRecipe r ->
       let cb = Term_typing.translate_recipe senv.env kn r in
       if DirPath.is_empty dir then Declareops.hcons_const_body cb else cb
-- 
cgit v1.2.3