Inductives in SProp, forbid primitive records with only sprop fields

For nonsquashed:
Either
- 0 constructors
- primitive record

3 files changed, 10 insertions, 11 deletions

diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index 8b8307c14a..977e804da2 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -140,9 +140,6 @@ let make_conclusion_flexible sigma = function
         | None -> sigma)
      | _ -> sigma)
 
-let is_impredicative env u =
-  Sorts.is_prop u || (is_impredicative_set env && Sorts.is_set u)
-
 let interp_ind_arity env sigma ind =
   let c = intern_gen IsType env sigma ind.ind_arity in
   let impls = Implicit_quantifiers.implicits_of_glob_constr ~with_products:true c in
@@ -177,7 +174,7 @@ let sign_level env evd sign =
         in
         let u = univ_of_sort s in
           (Univ.sup u lev, push_rel d env))
-    sign (Univ.type0m_univ,env))
+    sign (Univ.Universe.sprop,env))
 
 let sup_list min = List.fold_left Univ.sup min
 
@@ -261,7 +258,7 @@ let solve_constraints_system levels level_bounds =
 let inductive_levels env evd poly arities inds =
   let destarities = List.map (fun x -> x, Reduction.dest_arity env x) arities in
   let levels = List.map (fun (x,(ctx,a)) ->
-    if Sorts.is_prop a then None
+    if Sorts.is_prop a || Sorts.is_sprop a then None
     else Some (univ_of_sort a)) destarities
   in
   let cstrs_levels, min_levels, sizes =
@@ -270,7 +267,7 @@ let inductive_levels env evd poly arities inds =
         let len = List.length tys in
         let minlev = Sorts.univ_of_sort du in
         let minlev =
-          if len > 1 && not (is_impredicative env du) then
+          if len > 1 && not (is_impredicative_sort env du) then
             Univ.sup minlev Univ.type0_univ
           else minlev
         in
@@ -291,7 +288,7 @@ let inductive_levels env evd poly arities inds =
   in
   let evd, arities =
     CList.fold_left3 (fun (evd, arities) cu (arity,(ctx,du)) len ->
-      if is_impredicative env du then
+      if is_impredicative_sort env du then
         (* Any product is allowed here. *)
         evd, arity :: arities
       else (* If in a predicative sort, or asked to infer the type,
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index 0e0788c470..047bdd2b61 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -489,6 +489,8 @@ let explain_ill_formed_rec_body env sigma err names i fixenv vdefj =
      str "The return clause of the following pattern matching should be" ++
      strbrk " a coinductive type:" ++
      spc () ++ pr_lconstr_env env sigma c
+  | FixpointOnIrrelevantInductive ->
+    strbrk "Fixpoints on proof irrelevant inductive types should produce proof irrelevant values"
   in
   prt_name i ++ str " is ill-formed." ++ fnl () ++
   pr_ne_context_of (str "In environment") env sigma ++
@@ -1205,7 +1207,7 @@ let error_large_non_prop_inductive_not_in_type () =
   str "Large non-propositional inductive types must be in Type."
 
 let error_inductive_bad_univs () =
-  str "Incorrect universe constrains declared for inductive type."
+  str "Incorrect universe constraints declared for inductive type."
 
 (* Recursion schemes errors *)
 
diff --git a/vernac/record.ml b/vernac/record.ml
index 6b223f845b..46b4074eaa 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -92,7 +92,7 @@ let compute_constructor_level evars env l =
 	  Univ.sup (univ_of_sort s) univ 
       else univ
     in (EConstr.push_rel d env, univ))
-    l (env, Univ.type0m_univ)
+    l (env, Univ.Universe.sprop)
 
 let binder_of_decl = function
   | Vernacexpr.AssumExpr(n,t) -> (n,None,t)
@@ -167,8 +167,8 @@ let typecheck_params_and_fields finite def poly pl ps records =
     Pretyping.solve_remaining_evars Pretyping.all_and_fail_flags env_ar sigma in
   let fold sigma (typ, sort) (_, newfs) =
     let _, univ = compute_constructor_level sigma env_ar newfs in
-      if not def && (Sorts.is_prop sort ||
-	(Sorts.is_set sort && is_impredicative_set env0)) then
+    let univ = if Sorts.is_sprop sort then univ else Univ.Universe.sup univ Univ.type0m_univ in
+      if not def && is_impredicative_sort env0 sort then
         sigma, typ
       else
         let sigma = Evd.set_leq_sort env_ar sigma (Sorts.sort_of_univ univ) sort in