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, 9 insertions, 5 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 7f1dc70d95..5ede9d6a99 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -16,6 +16,7 @@ open Names
 open Nameops
 open Namegen
 open Constr
+open Context
 open Libnames
 open Globnames
 open Impargs
@@ -1020,6 +1021,7 @@ let sort_info_of_level_info (info: level_info) : (Libnames.qualid * int) option
 
 let glob_sort_of_level (level: glob_level) : glob_sort =
   match level with
+  | GSProp -> GSProp
   | GProp -> GProp
   | GSet -> GSet
   | GType info -> GType [sort_info_of_level_info info]
@@ -2182,7 +2184,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
                     (add_name match_acc CAst.(make ?loc x)) (CAst.make ?loc x::var_acc)
                 | _ ->
                   let fresh =
-                    Namegen.next_name_away_with_default_using_types "iV" cano_name forbidden_names (EConstr.of_constr ty) in
+                    Namegen.next_name_away_with_default_using_types "iV" cano_name.binder_name forbidden_names (EConstr.of_constr ty) in
                   canonize_args t tt (Id.Set.add fresh forbidden_names)
                     ((fresh,c)::match_acc) ((CAst.make ?loc:(cases_pattern_loc c) @@ Name fresh)::var_acc)
                 end
@@ -2431,9 +2433,10 @@ let interp_glob_context_evars ?(program_mode=false) env sigma k bl =
        in
        let sigma, t = understand_tcc ~flags env sigma ~expected_type:IsType t' in
 	match b with
-	    None ->
-	      let d = LocalAssum (na,t) in
-	      let impls =
+          None ->
+              let r = Retyping.relevance_of_type env sigma t in
+              let d = LocalAssum (make_annot na r,t) in
+              let impls =
 		if k == Implicit then
 		  let na = match na with Name n -> Some n | Anonymous -> None in
 		    (ExplByPos (n, na), (true, true, true)) :: impls
@@ -2442,7 +2445,8 @@ let interp_glob_context_evars ?(program_mode=false) env sigma k bl =
                 (push_rel d env, sigma, d::params, succ n, impls)
 	  | Some b ->
               let sigma, c = understand_tcc ~flags env sigma ~expected_type:(OfType t) b in
-	      let d = LocalDef (na, c, t) in
+              let r = Retyping.relevance_of_type env sigma t in
+              let d = LocalDef (make_annot na r, c, t) in
                 (push_rel d env, sigma, d::params, n, impls))
       (env,sigma,[],k+1,[]) (List.rev bl)
   in sigma, ((env, par), impls)