Merge PR #79: Let the kernel assume that a (co-)inductive type is positive.

1 files changed, 10 insertions, 10 deletions

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index ce05190b6..72d6ee518 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -373,8 +373,8 @@ let safe_push_named d env =
   Environ.push_named d env
 
 
-let push_named_def (id,de) senv =
-  let c,typ,univs = Term_typing.translate_local_def senv.revstruct senv.env id de in
+let push_named_def ~flags (id,de) senv =
+  let c,typ,univs = Term_typing.translate_local_def ~flags senv.revstruct senv.env id de in
   let poly = de.Entries.const_entry_polymorphic in
   let univs = Univ.ContextSet.of_context univs in
   let c, univs = match c with
@@ -388,9 +388,9 @@ let push_named_def (id,de) senv =
   let env'' = safe_push_named (LocalDef (id,c,typ)) senv'.env in
     univs, {senv' with env=env''}
 
-let push_named_assum ((id,t,poly),ctx) senv =
+let push_named_assum ~flags ((id,t,poly),ctx) senv =
   let senv' = push_context_set poly ctx senv in
-  let t = Term_typing.translate_local_assum senv'.env t in
+  let t = Term_typing.translate_local_assum ~flags senv'.env t in
   let env'' = safe_push_named (LocalAssum (id,t)) senv'.env in
     {senv' with env=env''}
 
@@ -479,7 +479,7 @@ let update_resolver f senv = { senv with modresolver = f senv.modresolver }
 
 (** Insertion of constants and parameters in environment *)
 type global_declaration =
-  | ConstantEntry of bool * private_constants Entries.constant_entry
+  | ConstantEntry of bool * private_constants Entries.constant_entry * Declarations.typing_flags
   | GlobalRecipe of Cooking.recipe
 
 type exported_private_constant = 
@@ -512,10 +512,10 @@ let add_constant dir l decl senv =
   let no_section = DirPath.is_empty dir in
   let seff_to_export, decl =
     match decl with
-    | ConstantEntry (true, ce) ->
+    | ConstantEntry (true, ce, flags) ->
         let exports, ce =
-          Term_typing.export_side_effects senv.revstruct senv.env ce in
-        exports, ConstantEntry (false, ce)
+          Term_typing.export_side_effects ~flags senv.revstruct senv.env ce in
+        exports, ConstantEntry (false, ce, flags)
     | _ -> [], decl
   in
   let senv =
@@ -524,8 +524,8 @@ let add_constant dir l decl senv =
   let senv =
     let cb = 
       match decl with
-      | ConstantEntry (export_seff,ce) ->
-        Term_typing.translate_constant senv.revstruct senv.env kn ce
+      | ConstantEntry (export_seff,ce,flags) ->
+        Term_typing.translate_constant ~flags senv.revstruct senv.env kn ce
       | GlobalRecipe r ->
         let cb = Term_typing.translate_recipe senv.env kn r in
         if no_section then Declareops.hcons_const_body cb else cb in