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

6 files changed, 19 insertions, 12 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 8e49800982..d5cb25d1fb 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -755,6 +755,7 @@ let extended_glob_local_binder_of_decl ?loc u = DAst.make ?loc (extended_glob_lo
 (* mapping glob_constr to constr_expr                                    *)
 
 let extern_glob_sort = function
+  | GSProp -> GSProp
   | GProp -> GProp
   | GSet -> GSet
   | GType _ as s when !print_universes -> s
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)
diff --git a/interp/declare.ml b/interp/declare.ml
index 4371b15c82..08a6ac5f7b 100644
--- a/interp/declare.ml
+++ b/interp/declare.ml
@@ -370,7 +370,7 @@ let declare_projections univs mind =
   let mib = Environ.lookup_mind mind env in
   match mib.mind_record with
   | PrimRecord info ->
-    let iter_ind i (_, labs, _) =
+    let iter_ind i (_, labs, _, _) =
       let ind = (mind, i) in
       let projs = Inductiveops.compute_projections env ind in
       Array.iter2_i (declare_one_projection univs ind ~proj_npars:mib.mind_nparams) labs projs
diff --git a/interp/discharge.ml b/interp/discharge.ml
index 353b0f6057..1efd13adb1 100644
--- a/interp/discharge.ml
+++ b/interp/discharge.ml
@@ -69,7 +69,7 @@ let refresh_polymorphic_type_of_inductive (_,mip) =
   | RegularArity s -> s.mind_user_arity, false
   | TemplateArity ar ->
     let ctx = List.rev mip.mind_arity_ctxt in
-      mkArity (List.rev ctx, Type ar.template_level), true
+      mkArity (List.rev ctx, Sorts.sort_of_univ ar.template_level), true
 
 let process_inductive info modlist mib =
   let section_decls = Lib.named_of_variable_context info.Lib.abstr_ctx in
@@ -103,7 +103,7 @@ let process_inductive info modlist mib =
   let (params',inds') = abstract_inductive section_decls' nparamdecls inds in
   let record = match mib.mind_record with
     | PrimRecord info ->
-      Some (Some (Array.map pi1 info))
+      Some (Some (Array.map (fun (x,_,_,_) -> x) info))
     | FakeRecord -> Some None
     | NotRecord -> None
   in
diff --git a/interp/impargs.ml b/interp/impargs.ml
index 0f9bff7f1d..d83a0ce918 100644
--- a/interp/impargs.ml
+++ b/interp/impargs.ml
@@ -243,7 +243,7 @@ let compute_implicits_names_gen all env sigma t =
     let t = whd_all env sigma t in
     match kind sigma t with
     | Prod (na,a,b) ->
-       let na',avoid' = find_displayed_name_in sigma all avoid na (names,b) in
+       let na',avoid' = find_displayed_name_in sigma all avoid na.Context.binder_name (names,b) in
        aux (push_rel (LocalAssum (na,a)) env) avoid' (na'::names) b
     | _ -> List.rev names
   in aux env Id.Set.empty [] t
@@ -445,7 +445,8 @@ let compute_mib_implicits flags kn =
         (fun i mip ->
           (* No need to care about constraints here *)
           let ty, _ = Typeops.type_of_global_in_context env (IndRef (kn,i)) in
-	  Context.Rel.Declaration.LocalAssum (Name mip.mind_typename, ty))
+          let r = Inductive.relevance_of_inductive env (kn,i) in
+          Context.Rel.Declaration.LocalAssum (Context.make_annot (Name mip.mind_typename) r, ty))
         mib.mind_packets) in
   let env_ar = Environ.push_rel_context ar env in
   let imps_one_inductive i mip =
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index 4f3037b1fc..854651e7b7 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -10,6 +10,7 @@
 
 (*i*)
 open Names
+open Context
 open Decl_kinds
 open CErrors
 open Util
@@ -175,10 +176,10 @@ let combine_params avoid fn applied needed =
     match app, need with
 	[], [] -> List.rev ids, avoid
 
-      | app, (_, (LocalAssum (Name id, _) | LocalDef (Name id, _, _))) :: need when Id.List.mem_assoc id named ->
+      | app, (_, (LocalAssum ({binder_name=Name id}, _) | LocalDef ({binder_name=Name id}, _, _))) :: need when Id.List.mem_assoc id named ->
 	  aux (Id.List.assoc id named :: ids) avoid app need
 
-      | (x, None) :: app, (None, (LocalAssum (Name id, _) | LocalDef (Name id, _, _))) :: need ->
+      | (x, None) :: app, (None, (LocalAssum ({binder_name=Name id}, _) | LocalDef ({binder_name=Name id}, _, _))) :: need ->
 	  aux (x :: ids) avoid app need
 
       | _, (Some cl, _ as d) :: need ->