Disable and remove Automatic Proposition Inductives

doc/changelog/08-vernac-commands-and-options/19872-depr-auto-prop-lowering.rst

@@ -0,0 +1,4 @@
+- **Removed:**
+  flag `Automatic Proposition Inductives` (using its effect was deprecated since 8.20)
+  (`#19872 <https://github.com/coq/coq/pull/19872>`_,
+  by Gaëtan Gilbert).

doc/sphinx/changes.rst

@@ -524,9 +524,8 @@ Ltac2 language
   (`#18988 <https://github.com/coq/coq/pull/18988>`_,
   by Gaëtan Gilbert).
 - **Added:**
-  :flag:`Automatic Proposition Inductives`, :flag:`Dependent Proposition Eliminators` and
-  :warn:`warning when automatically lowering an inductive declared with Type to Prop
-  <automatic-prop-lowering>`
+  flag `Automatic Proposition Inductives`, :flag:`Dependent Proposition Eliminators` and
+  warning `automatic-prop-lowering`
   (`#18989 <https://github.com/coq/coq/pull/18989>`_,
   by Gaëtan Gilbert).
 - **Added:**

doc/sphinx/language/core/inductive.rst

@@ -170,29 +170,6 @@ smallest sort which permits large elimination (excluding
 `SProp`). For :ref:`empty and singleton <Empty-and-singleton-elimination>`
 types this means they are declared in `Prop`.
 
-.. flag:: Automatic Proposition Inductives
-
-   By default the above behaviour is extended to empty and singleton
-   inductives explicitly declared in `Type` (but not those in explicit
-   universes using `Type@{u}`, or in `Type` through an auxiliary definition
-   such as `Definition typ := Type.`).
-
-   Disabling this flag prevents inductives with an explicit non-`Prop`
-   type from being lowered to `Prop`. This will become the default in
-   a future version. Use :flag:`Dependent Proposition Eliminators` to
-   declare the inductive type in `Prop` while preserving compatibility.
-
-   Depending on universe minimization they may then be declared in
-   `Set` or in a floating universe level,
-   see also :flag:`Universe Minimization ToSet`.
-
-.. warn:: Automatically putting @ident in Prop even though it was declared with Type.
-   :name: automatic-prop-lowering
-
-   This warning is produced when :flag:`Automatic Proposition
-   Inductives` is enabled and resulted in an inductive type being
-   lowered to `Prop`.
-
 Simple indexed inductive types
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 

plugins/funind/glob_term_to_relation.ml

@@ -1522,7 +1522,6 @@ let do_build_inductive evd (funconstants : pconstant list)
       ComInductive.poly = false;
       cumulative = false;
       template = Some false;
-      auto_prop_lowering = false;
       finite = Finite;
       mode = None;
     }

test-suite/bugs/bug_19872.v

@@ -0,0 +1,5 @@
+Polymorphic Inductive eq@{s s'|l +|} {A:Type@{s|l}} (x:A) : A -> Type@{s'|_} :=
+  eq_refl : eq x x.
+
+Check eq 0 0 : SProp.
+Check eq 0 0 : Prop.

test-suite/success/AutoPropLowering.v

@@ -1,8 +1,3 @@
-Set Warnings "+automatic-prop-lowering".
-
-Fail Inductive foo : Type := .
-
-Unset Automatic Proposition Inductives.
 
 Inductive foo : Type := .
 

vernac/comInductive.ml

@@ -33,7 +33,6 @@ type flags = {
   poly : bool;
   cumulative : bool;
   template : bool option;
-  auto_prop_lowering : bool;
   finite : Declarations.recursivity_kind;
   mode : Hints.hint_mode list option;
 }
@@ -213,24 +212,14 @@ let compute_constructor_levels env evd sign =
           (s :: lev, EConstr.push_rel d env))
     sign ([],env))
 
-let warn_auto_prop_lowering =
-  CWarnings.create ~name:"automatic-prop-lowering" ~category:Deprecation.Version.v8_20
-    Pp.(fun na ->
-        strbrk "Automatically putting " ++ Id.print na ++ strbrk " in Prop" ++ spc() ++
-        strbrk "even though it was declared with Type." ++ fnl() ++
-        strbrk "Unset Automatic Proposition Inductives to prevent this" ++ spc() ++
-        strbrk "(it will become the default in a future version)." ++ fnl() ++
-        strbrk "If you instead put " ++ Id.print na ++ strbrk " explicitly in Prop," ++ spc() ++
-        strbrk "set Dependent Proposition Eliminators around the declaration for full backwards compatibility.")
-
 let is_flexible_sort evd s = match ESorts.kind evd s with
 | Set | Prop | SProp -> false
 | Type u | QSort (_, u) ->
   match Univ.Universe.level u with
   | Some l -> Evd.is_flexible_level evd l
   | None -> false
 
-let prop_lowering_candidates ~auto_prop_lowering evd ~arities_explicit inds =
+let prop_lowering_candidates evd ~arities_explicit inds =
   let less_than_2 = function [] | [_] -> true | _ :: _ :: _ -> false in
 
   (* handle automatic lowering to Prop
@@ -244,7 +233,7 @@ let prop_lowering_candidates ~auto_prop_lowering evd ~arities_explicit inds =
     && not (Evd.check_leq evd ESorts.set s)
   in
   let candidates = List.filter_map (fun (explicit,(_,(_,s),_,_ as ind)) ->
-      if (auto_prop_lowering || not explicit) && is_prop_candidate_arity ind
+      if (not explicit) && is_prop_candidate_arity ind
       then Some s else None)
       (List.combine arities_explicit inds)
   in
@@ -303,7 +292,7 @@ let include_constructor_argument env evd ~poly ~ctor_sort ~inductive_sort =
 
 type default_dep_elim = DeclareInd.default_dep_elim = DefaultElim | PropButDepElim
 
-let inductive_levels ~auto_prop_lowering env evd ~poly ~indnames ~arities_explicit arities ctors =
+let inductive_levels env evd ~poly ~indnames ~arities_explicit arities ctors =
   let inds = List.map2 (fun x ctors ->
       let ctx, s = Reductionops.dest_arity env evd x in
       x, (ctx, s), List.map (compute_constructor_levels env evd) ctors)
@@ -332,7 +321,7 @@ let inductive_levels ~auto_prop_lowering env evd ~poly ~indnames ~arities_explic
       inds
   in
 
-  let candidates = prop_lowering_candidates ~auto_prop_lowering evd ~arities_explicit inds in
+  let candidates = prop_lowering_candidates evd ~arities_explicit inds in
   (* Do the lowering. We forget about the generated universe for the
      lowered inductive and rely on universe restriction to get rid of
      it.
@@ -348,7 +337,6 @@ let inductive_levels ~auto_prop_lowering env evd ~poly ~indnames ~arities_explic
       if List.mem_f (ESorts.equal evd) s candidates then
         (* NB: is_prop_candidate requires is_flexible_sort
            so in this branch we know s <> Prop *)
-        let () = if explicit then warn_auto_prop_lowering na in
         ((PropButDepElim, mkArity (ctx, ESorts.prop)),ESorts.prop,indices,ctors)
       else ((DefaultElim, raw_arity), s, indices, ctors))
       indnames
@@ -545,7 +533,6 @@ let interp_mutual_inductive_constr ~sigma ~flags ~udecl ~variances ~ctx_params ~
     poly;
     cumulative;
     template;
-    auto_prop_lowering;
     finite;
   } = flags in
   (* Compute renewed arities *)
@@ -556,7 +543,7 @@ let interp_mutual_inductive_constr ~sigma ~flags ~udecl ~variances ~ctx_params ~
         tys)
       constructors
   in
-  let sigma, (default_dep_elim, arities) = inductive_levels ~auto_prop_lowering env_ar_params sigma ~poly ~indnames ~arities_explicit arities ctor_args in
+  let sigma, (default_dep_elim, arities) = inductive_levels env_ar_params sigma ~poly ~indnames ~arities_explicit arities ctor_args in
   let lbound = if poly then UGraph.Bound.Set else UGraph.Bound.Prop in
   let sigma = Evd.minimize_universes ~lbound sigma in
   let arities = List.map EConstr.(to_constr sigma) arities in

vernac/comInductive.mli

@@ -17,7 +17,6 @@ type flags = {
   poly : bool;
   cumulative : bool;
   template : bool option;
-  auto_prop_lowering : bool;
   finite : Declarations.recursivity_kind;
   mode : Hints.hint_mode list option;
 }
@@ -130,8 +129,7 @@ sig
   (** Returns the modified arities (the result sort may be replaced by Prop).
       Should be called with minimized universes. *)
   val inductive_levels
-    : auto_prop_lowering:bool
-    -> Environ.env
+    : Environ.env
     -> Evd.evar_map
     -> poly:bool
     -> indnames:Names.Id.t list

vernac/record.ml

@@ -216,7 +216,7 @@ let def_class_levels ~def env_ar sigma aritysorts ctors =
     sigma, [DefaultElim, EConstr.mkSort s]
 
 (* ps = parameter list *)
-let typecheck_params_and_fields ~auto_prop_lowering def ~poly udecl ps (records : DataI.t list) : tc_result =
+let typecheck_params_and_fields def ~poly udecl ps (records : DataI.t list) : tc_result =
   let env0 = Global.env () in
   (* Special case elaboration for template-polymorphic inductives,
      lower bound on introduced universes is Prop so that we do not miss
@@ -256,7 +256,7 @@ let typecheck_params_and_fields ~auto_prop_lowering def ~poly udecl ps (records
       let indnames = List.map (fun x -> x.DataI.name) records in
       let arities_explicit = List.map (fun x -> Option.has_some x.DataI.arity) records in
       let sigma, (default_dep_elim, typs) =
-        ComInductive.Internal.inductive_levels ~auto_prop_lowering env_ar sigma ~poly ~indnames ~arities_explicit typs ctors
+        ComInductive.Internal.inductive_levels env_ar sigma ~poly ~indnames ~arities_explicit typs ctors
       in
       sigma, List.combine default_dep_elim typs
   in
@@ -716,7 +716,7 @@ let check_proj_flags kind rf =
   let pf_canonical = rf.rf_canonical in
   Data.{ pf_coercion; pf_reversible; pf_instance; pf_priority; pf_locality; pf_canonical }
 
-let pre_process_structure ~auto_prop_lowering udecl kind ~poly (records : Ast.t list) =
+let pre_process_structure udecl kind ~poly (records : Ast.t list) =
   let indlocs = check_unique_names records in
   let () = check_priorities kind records in
   let ps, data = extract_record_data records in
@@ -727,7 +727,7 @@ let pre_process_structure ~auto_prop_lowering udecl kind ~poly (records : Ast.t
        is messing state beyond that.
     *)
     Vernacstate.System.protect (fun () ->
-        typecheck_params_and_fields ~auto_prop_lowering (kind = Class true) ~poly udecl ps data) ()
+        typecheck_params_and_fields (kind = Class true) ~poly udecl ps data) ()
   in
   let adjust_impls impls = match kind_class kind with
     | NotClass -> impargs @ [CAst.make None] @ impls
@@ -816,11 +816,10 @@ let interp_structure ~flags udecl kind ~primitive_proj records =
       poly;
       cumulative;
       template;
-      auto_prop_lowering;
       finite;
     } = flags in
   let impargs, params, univs, variances, projections_kind, data, indlocs =
-    pre_process_structure ~auto_prop_lowering udecl kind ~poly records in
+    pre_process_structure udecl kind ~poly records in
   interp_structure_core ~cumulative finite ~univs ~variances ~primitive_proj impargs params template ~projections_kind ~indlocs data
 
 let declare_structure { Record_decl.mie; default_dep_elim; primitive_proj; impls; globnames; global_univ_decls; projunivs; ubinders; projections_kind; poly; records; indlocs } =
@@ -1049,11 +1048,10 @@ let definition_structure ~flags udecl kind ~primitive_proj (records : Ast.t list
       poly;
       cumulative;
       template;
-      auto_prop_lowering;
       finite;
     } = flags in
   let impargs, params, univs, variances, projections_kind, data, indlocs =
-    pre_process_structure ~auto_prop_lowering udecl kind ~poly records
+    pre_process_structure udecl kind ~poly records
   in
   let inds, def = match kind_class kind with
     | DefClass -> declare_class_constant ~univs impargs params data

vernac/vernacentries.ml

@@ -1030,9 +1030,6 @@ let primitive_proj =
   | Some t -> return t
   | None -> return (primitive_flag ())
 
-let { Goptions.get = do_auto_prop_lowering } =
-  Goptions.declare_bool_option_and_ref ~key:["Automatic";"Proposition";"Inductives"] ~value:true ()
-
 let mode_attr =
   let open Attributes in
   let open Notations in
@@ -1096,8 +1093,7 @@ let preprocess_inductive_decl ~atts kind indl =
           ++ private_ind ++ typing_flags ++ prim_proj_attr ++ hint_mode_attr)
         atts)
   in
-  let auto_prop_lowering = do_auto_prop_lowering () in
-  let flags = { ComInductive.template; cumulative; poly; finite; auto_prop_lowering; mode } in
+  let flags = { ComInductive.template; cumulative; poly; finite; mode } in
   if Option.has_some is_defclass then
     (* Definitional class case *)
     let (id, bl, c, l) = Option.get is_defclass in