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.

4 files changed, 17 insertions, 13 deletions

diff --git a/library/declare.ml b/library/declare.ml
index 02e6dadde..4be13109a 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -50,11 +50,11 @@ let cache_variable ((sp,_),o) =
 
   let impl,opaq,poly,ctx = match d with (* Fails if not well-typed *)
     | SectionLocalAssum ((ty,ctx),poly,impl) ->
-      let () = Global.push_named_assum ((id,ty),ctx) in
+      let () = Global.push_named_assum ~chkguard:true ((id,ty),ctx) in
       let impl = if impl then Implicit else Explicit in
 	impl, true, poly, ctx
     | SectionLocalDef (de) ->
-      let () = Global.push_named_def (id,de) in
+      let () = Global.push_named_def ~chkguard:true (id,de) in
         Explicit, de.const_entry_opaque, de.const_entry_polymorphic, 
 	(Univ.ContextSet.of_context de.const_entry_universes) in
   Nametab.push (Nametab.Until 1) (restrict_path 0 sp) (VarRef id);
@@ -156,7 +156,7 @@ let discharge_constant ((sp, kn), obj) =
 
 (* Hack to reduce the size of .vo: we keep only what load/open needs *)
 let dummy_constant_entry = 
-  ConstantEntry (ParameterEntry (None,false,(mkProp,Univ.UContext.empty),None))
+  ConstantEntry (ParameterEntry (None,false,(mkProp,Univ.UContext.empty),None), true)
 
 let dummy_constant cst = {
   cst_decl = dummy_constant_entry;
@@ -232,7 +232,7 @@ let declare_sideff env fix_exn se =
         const_entry_feedback = None;
 	const_entry_polymorphic = cb.const_polymorphic;
 	const_entry_universes = univs;
-    });
+      }, true);
     cst_hyps = [] ;
     cst_kind =  Decl_kinds.IsDefinition Decl_kinds.Definition;
     cst_locl = true;
@@ -253,7 +253,7 @@ let declare_sideff env fix_exn se =
                if Constant.equal c c' then Some (x,kn) else None) inds_consts)
            knl))
 
-let declare_constant ?(internal = UserVerbose) ?(local = false) id ?(export_seff=false) (cd, kind) =
+let declare_constant ?(chkguard=true) ?(internal = UserVerbose) ?(local = false) id ?(export_seff=false) (cd, kind) =
   let cd = (* We deal with side effects *)
     match cd with
     | Entries.DefinitionEntry de ->
@@ -275,7 +275,7 @@ let declare_constant ?(internal = UserVerbose) ?(local = false) id ?(export_seff
     | _ -> cd
   in
   let cst = {
-    cst_decl = ConstantEntry cd;
+    cst_decl = ConstantEntry (cd,chkguard);
     cst_hyps = [] ;
     cst_kind = kind;
     cst_locl = local;
@@ -283,13 +283,13 @@ let declare_constant ?(internal = UserVerbose) ?(local = false) id ?(export_seff
   let kn = declare_constant_common id cst in
   kn
 
-let declare_definition ?(internal=UserVerbose) 
+let declare_definition ?chkguard ?(internal=UserVerbose) 
   ?(opaque=false) ?(kind=Decl_kinds.Definition) ?(local = false)
   ?(poly=false) id ?types (body,ctx) =
   let cb = 
     definition_entry ?types ~poly ~univs:(Univ.ContextSet.to_context ctx) ~opaque body
   in
-    declare_constant ~internal ~local id
+    declare_constant ?chkguard ~internal ~local id
       (Entries.DefinitionEntry cb, Decl_kinds.IsDefinition kind)
 
 (** Declaration of inductive blocks *)
@@ -387,7 +387,7 @@ let declare_projections mind =
       Array.iteri (fun i kn -> 
 	let id = Label.to_id (Constant.label kn) in
 	let entry = {proj_entry_ind = mind; proj_entry_arg = i} in
-	let kn' = declare_constant id (ProjectionEntry entry,
+	let kn' = declare_constant ~chkguard:true id (ProjectionEntry entry,
 				       IsDefinition StructureComponent) 
 	in
 	  assert(eq_constant kn kn')) kns; true
diff --git a/library/declare.mli b/library/declare.mli
index d8a00db0c..94cebe3bd 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
diff --git a/library/global.ml b/library/global.ml
index 49fa2ef28..27f7f5266 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -77,8 +77,8 @@ let globalize_with_summary fs f =
 
 let i2l = Label.of_id
 
-let push_named_assum a = globalize0 (Safe_typing.push_named_assum a)
-let push_named_def d = globalize0 (Safe_typing.push_named_def d)
+let push_named_assum ~chkguard a = globalize0 (Safe_typing.push_named_assum ~chkguard a)
+let push_named_def ~chkguard d = globalize0 (Safe_typing.push_named_def ~chkguard d)
 let add_constraints c = globalize0 (Safe_typing.add_constraints c)
 let push_context_set c = globalize0 (Safe_typing.push_context_set c)
 let push_context c = globalize0 (Safe_typing.push_context c)
diff --git a/library/global.mli b/library/global.mli
index 248e1f86d..388fee527 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -31,8 +31,10 @@ val set_type_in_type : unit -> unit
 
 (** Variables, Local definitions, constants, inductive types *)
 
-val push_named_assum : (Id.t * Constr.types) Univ.in_universe_context_set -> unit
-val push_named_def   : (Id.t * Entries.definition_entry) -> unit
+val push_named_assum : 
+  chkguard:bool -> (Id.t * Constr.types) Univ.in_universe_context_set -> unit
+val push_named_def   :
+  chkguard:bool -> (Id.t * Entries.definition_entry) -> unit
 
 val add_constant :
   DirPath.t -> Id.t -> Safe_typing.global_declaration -> constant