Merge PR #8817: SProp: the definitionally proof irrelevant universe

Ack-by: JasonGross
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
Ack-by: gares
Ack-by: mattam82

1 files changed, 13 insertions, 7 deletions

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index a05f7b9b04..edb1d0a02e 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -211,6 +211,10 @@ let set_native_compiler b senv =
   let flags = Environ.typing_flags senv.env in
   set_typing_flags { flags with enable_native_compiler = b } senv
 
+let make_sprop_cumulative senv = { senv with env = Environ.make_sprop_cumulative senv.env }
+
+let set_allow_sprop b senv = { senv with env = Environ.set_allow_sprop b senv.env }
+
 (** Check that the engagement [c] expected by a library matches
     the current (initial) one *)
 let check_engagement env expected_impredicative_set =
@@ -437,14 +441,16 @@ let safe_push_named d env =
 
 
 let push_named_def (id,de) senv =
-  let c, typ = Term_typing.translate_local_def senv.env id de in
-  let env'' = safe_push_named (LocalDef (id, c, typ)) senv.env in
+  let c, r, typ = Term_typing.translate_local_def senv.env id de in
+  let x = Context.make_annot id r in
+  let env'' = safe_push_named (LocalDef (x, c, typ)) senv.env in
   { senv with env = env'' }
 
 let push_named_assum ((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 env'' = safe_push_named (LocalAssum (id,t)) senv'.env in
+  let t, r = Term_typing.translate_local_assum senv'.env t in
+  let x = Context.make_annot id r in
+  let env'' = safe_push_named (LocalAssum (x,t)) senv'.env in
     {senv' with env=env''}
 
 
@@ -603,7 +609,7 @@ let inline_side_effects env body side_eff =
   if List.is_empty side_eff then (body, Univ.ContextSet.empty, sigs)
   else
     (** Second step: compute the lifts and substitutions to apply *)
-    let cname c = Name (Label.to_id (Constant.label c)) in
+    let cname c r = Context.make_annot (Name (Label.to_id (Constant.label c))) r in
     let fold (subst, var, ctx, args) (c, cb, b) =
       let (b, opaque) = match cb.const_body, b with
       | Def b, _ -> (Mod_subst.force_constr b, false)
@@ -616,7 +622,7 @@ let inline_side_effects env body side_eff =
         let ty = cb.const_type in
         let subst = Cmap_env.add c (Inr var) subst in
         let ctx = Univ.ContextSet.union ctx univs in
-        (subst, var + 1, ctx, (cname c, b, ty, opaque) :: args)
+        (subst, var + 1, ctx, (cname c cb.const_relevance, b, ty, opaque) :: args)
       | Polymorphic _ ->
         (** Inline the term to emulate universe polymorphism *)
         let subst = Cmap_env.add c (Inl b) subst in
@@ -1239,7 +1245,7 @@ let check_register_ind ind r env =
       check_if (Constr.is_Type d) s;
       check_if
         (Constr.equal
-                (mkProd (Anonymous,mkRel 1, mkApp (mkRel 3,[|mkRel 2|])))
+                (mkProd (Context.anonR,mkRel 1, mkApp (mkRel 3,[|mkRel 2|])))
                 cd)
         s in
     check_name 0 "C0";