aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--CHANGES.md2
-rw-r--r--doc/sphinx/language/gallina-extensions.rst9
-rw-r--r--gramlib/grammar.ml3
-rw-r--r--interp/notation_ops.ml5
-rw-r--r--lib/dAst.ml2
-rw-r--r--lib/dAst.mli1
-rw-r--r--lib/flags.ml4
-rw-r--r--lib/flags.mli4
-rw-r--r--plugins/extraction/extraction.ml59
-rw-r--r--plugins/funind/glob_term_to_relation.ml10
-rw-r--r--pretyping/detyping.ml42
-rw-r--r--pretyping/glob_ops.ml10
-rw-r--r--pretyping/glob_ops.mli1
-rw-r--r--pretyping/inductiveops.ml29
-rw-r--r--pretyping/inductiveops.mli8
-rw-r--r--test-suite/bugs/closed/bug_5197.v2
-rw-r--r--test-suite/output/Notations4.out20
-rw-r--r--test-suite/output/Notations4.v9
-rw-r--r--test-suite/success/Notations2.v11
-rw-r--r--vernac/vernacentries.ml15
20 files changed, 129 insertions, 117 deletions
diff --git a/CHANGES.md b/CHANGES.md
index d0774276ad..38c197d8cc 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -194,6 +194,8 @@ Misc
- Option "Typeclasses Axioms Are Instances" is deprecated. Use Declare Instance for axioms which should be instances.
+- Removed option "Printing Primitive Projection Compatibility"
+
SSReflect
- New intro patterns:
diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index 2f99368f48..25f983ac1e 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -247,11 +247,6 @@ Primitive Projections
printing time (even though they are absent in the actual AST manipulated
by the kernel).
-.. flag:: Printing Primitive Projection Compatibility
-
- This compatibility option (on by default) governs the
- printing of pattern matching over primitive records.
-
Primitive Record Types
++++++++++++++++++++++
@@ -297,8 +292,8 @@ the folded version delta-reduces to the unfolded version. This allows to
precisely mimic the usual unfolding rules of constants. Projections
obey the usual ``simpl`` flags of the ``Arguments`` command in particular.
There is currently no way to input unfolded primitive projections at the
-user-level, and one must use the :flag:`Printing Primitive Projection Compatibility`
-to display unfolded primitive projections as matches and distinguish them from folded ones.
+user-level, and there is no way to display unfolded projections differently
+from folded ones.
Compatibility Projections and :g:`match`
diff --git a/gramlib/grammar.ml b/gramlib/grammar.ml
index e313f2e648..f46ddffd6e 100644
--- a/gramlib/grammar.ml
+++ b/gramlib/grammar.ml
@@ -1368,6 +1368,9 @@ let parse_parsable entry p =
let get_loc () =
try
let cnt = Stream.count ts in
+ (* Ensure that the token at location cnt has been peeked so that
+ the location function knows about it *)
+ let _ = Stream.peek ts in
let loc = fun_loc cnt in
if !token_count - 1 <= cnt then loc
else Loc.merge loc (fun_loc (!token_count - 1))
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 890c24e633..7d7e10a05b 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -908,11 +908,8 @@ let bind_term_as_binding_env alp (terms,termlists,binders,binderlists as sigma)
(* TODO: look at the consequences for alp *)
alp, add_env alp sigma var (DAst.make @@ GVar id)
-let force_cases_pattern c =
- DAst.make ?loc:c.CAst.loc (DAst.get c)
-
let bind_binding_as_term_env alp (terms,termlists,binders,binderlists as sigma) var c =
- let pat = try force_cases_pattern (cases_pattern_of_glob_constr Anonymous c) with Not_found -> raise No_match in
+ let pat = try cases_pattern_of_glob_constr Anonymous c with Not_found -> raise No_match in
try
(* If already bound to a binder, unify the term and the binder *)
let patl' = Id.List.assoc var binders in
diff --git a/lib/dAst.ml b/lib/dAst.ml
index f34ab956a3..803b2a0cff 100644
--- a/lib/dAst.ml
+++ b/lib/dAst.ml
@@ -30,6 +30,8 @@ let make ?loc v = CAst.make ?loc (Value v)
let delay ?loc v = CAst.make ?loc (Thunk (Lazy.from_fun v))
+let force x = CAst.make ?loc:x.CAst.loc (Value (get_thunk x.v))
+
let map f n = CAst.map (fun x -> map_thunk f x) n
let map_with_loc f n =
diff --git a/lib/dAst.mli b/lib/dAst.mli
index 28c78784e6..2f58cfc41f 100644
--- a/lib/dAst.mli
+++ b/lib/dAst.mli
@@ -21,6 +21,7 @@ val get_thunk : ('a, 'b) thunk -> 'a
val make : ?loc:Loc.t -> 'a -> ('a, 'b) t
val delay : ?loc:Loc.t -> (unit -> 'a) -> ('a, [ `thunk ]) t
+val force : ('a, 'b) t -> ('a, 'b) t
val map : ('a -> 'b) -> ('a, 'c) t -> ('b, 'c) t
val map_with_loc : (?loc:Loc.t -> 'a -> 'b) -> ('a, 'c) t -> ('b, 'c) t
diff --git a/lib/flags.ml b/lib/flags.ml
index 768d359cce..1195b8caf1 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -101,10 +101,6 @@ let verbosely f x = without_option quiet f x
let if_silent f x = if !quiet then f x
let if_verbose f x = if not !quiet then f x
-let polymorphic_inductive_cumulativity = ref false
-let make_polymorphic_inductive_cumulativity b = polymorphic_inductive_cumulativity := b
-let is_polymorphic_inductive_cumulativity () = !polymorphic_inductive_cumulativity
-
let warn = ref true
let make_warn flag = warn := flag; ()
let if_warn f x = if !warn then f x
diff --git a/lib/flags.mli b/lib/flags.mli
index 4ef5fb4445..2b4446a1db 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -75,10 +75,6 @@ val verbosely : ('a -> 'b) -> 'a -> 'b
val if_silent : ('a -> unit) -> 'a -> unit
val if_verbose : ('a -> unit) -> 'a -> unit
-(** Global polymorphic inductive cumulativity flag. *)
-val make_polymorphic_inductive_cumulativity : bool -> unit
-val is_polymorphic_inductive_cumulativity : unit -> bool
-
val warn : bool ref
val make_warn : bool -> unit
val if_warn : ('a -> unit) -> 'a -> unit
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index c15486ea10..204f889f90 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -1032,6 +1032,55 @@ let extract_fixpoint env sg vkn (fi,ti,ci) =
current_fixpoints := [];
Dfix (Array.map (fun kn -> ConstRef kn) vkn, terms, types)
+(** Because of automatic unboxing the easy way [mk_def c] on the
+ constant body of primitive projections doesn't work. We pretend
+ that they are implemented by matches until someone figures out how
+ to clean it up (test with #4710 when working on this). *)
+let fake_match_projection env p =
+ let ind = Projection.Repr.inductive p in
+ let proj_arg = Projection.Repr.arg p in
+ let mib, mip = Inductive.lookup_mind_specif env ind in
+ let u = Univ.make_abstract_instance (Declareops.inductive_polymorphic_context mib) in
+ let indu = mkIndU (ind,u) in
+ let ctx, paramslet =
+ let subst = List.init mib.mind_ntypes (fun i -> mkIndU ((fst ind, mib.mind_ntypes - i - 1), u)) in
+ let rctx, _ = decompose_prod_assum (Vars.substl subst mip.mind_nf_lc.(0)) in
+ List.chop mip.mind_consnrealdecls.(0) rctx
+ in
+ let ci_pp_info = { ind_tags = []; cstr_tags = [|Context.Rel.to_tags ctx|]; style = LetStyle } in
+ let ci = {
+ ci_ind = ind;
+ ci_npar = mib.mind_nparams;
+ ci_cstr_ndecls = mip.mind_consnrealdecls;
+ ci_cstr_nargs = mip.mind_consnrealargs;
+ ci_pp_info;
+ }
+ in
+ let x = match mib.mind_record with
+ | NotRecord | FakeRecord -> assert false
+ | PrimRecord info -> Name (pi1 info.(snd ind))
+ in
+ let indty = mkApp (indu, Context.Rel.to_extended_vect mkRel 0 paramslet) in
+ let rec fold arg j subst = function
+ | [] -> assert false
+ | LocalAssum (na,ty) :: rem ->
+ let ty = Vars.substl subst (liftn 1 j ty) in
+ if arg != proj_arg then
+ let lab = match na with Name id -> Label.of_id id | Anonymous -> assert false in
+ let kn = Projection.Repr.make ind ~proj_npars:mib.mind_nparams ~proj_arg:arg lab in
+ fold (arg+1) (j+1) (mkProj (Projection.make kn false, mkRel 1)::subst) rem
+ else
+ let p = mkLambda (x, lift 1 indty, liftn 1 2 ty) in
+ let branch = lift 1 (it_mkLambda_or_LetIn (mkRel (List.length ctx - (j-1))) ctx) in
+ let body = mkCase (ci, p, mkRel 1, [|branch|]) in
+ it_mkLambda_or_LetIn (mkLambda (x,indty,body)) mib.mind_params_ctxt
+ | LocalDef (_,c,t) :: rem ->
+ let c = liftn 1 j c in
+ let c1 = Vars.substl subst c in
+ fold arg (j+1) (c1::subst) rem
+ in
+ fold 0 1 [] (List.rev ctx)
+
let extract_constant env kn cb =
let sg = Evd.from_env env in
let r = ConstRef kn in
@@ -1069,10 +1118,7 @@ let extract_constant env kn cb =
(match Recordops.find_primitive_projection kn with
| None -> mk_typ (get_body c)
| Some p ->
- let p = Projection.make p false in
- let ind = Projection.inductive p in
- let bodies = Inductiveops.legacy_match_projection env ind in
- let body = bodies.(Projection.arg p) in
+ let body = fake_match_projection env p in
mk_typ (EConstr.of_constr body))
| OpaqueDef c ->
add_opaque r;
@@ -1085,10 +1131,7 @@ let extract_constant env kn cb =
(match Recordops.find_primitive_projection kn with
| None -> mk_def (get_body c)
| Some p ->
- let p = Projection.make p false in
- let ind = Projection.inductive p in
- let bodies = Inductiveops.legacy_match_projection env ind in
- let body = bodies.(Projection.arg p) in
+ let body = fake_match_projection env p in
mk_def (EConstr.of_constr body))
| OpaqueDef c ->
add_opaque r;
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 02964d7ba5..ba0a3bbb5c 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -321,12 +321,10 @@ let build_constructors_of_type ind' argl =
construct
in
let argl =
- if List.is_empty argl
- then
- Array.to_list
- (Array.init (cst_narg - npar) (fun _ -> mkGHole ())
- )
- else argl
+ if List.is_empty argl then
+ List.make cst_narg (mkGHole ())
+ else
+ List.make npar (mkGHole ()) @ argl
in
let pat_as_term =
mkGApp(mkGRef (ConstructRef(ind',i+1)),argl)
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 6746e4b902..99cd89cc2a 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -8,8 +8,6 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
-module CVars = Vars
-
open Pp
open CErrors
open Util
@@ -175,16 +173,6 @@ let () = declare_bool_option
optread = print_primproj_params;
optwrite = (:=) print_primproj_params_value }
-let print_primproj_compatibility_value = ref false
-let print_primproj_compatibility () = !print_primproj_compatibility_value
-
-let () = declare_bool_option
- { optdepr = false;
- optname = "backwards-compatible printing of primitive projections";
- optkey = ["Printing";"Primitive";"Projection";"Compatibility"];
- optread = print_primproj_compatibility;
- optwrite = (:=) print_primproj_compatibility_value }
-
(* Auxiliary function for MutCase printing *)
(* [computable] tries to tell if the predicate typing the result is inferable*)
@@ -702,30 +690,12 @@ and detype_r d flags avoid env sigma t =
GApp (DAst.make @@ GRef (ConstRef (Projection.constant p), None),
[detype d flags avoid env sigma c])
else
- if print_primproj_compatibility () && Projection.unfolded p then
- (* Print the compatibility match version *)
- let c' =
- try
- let ind = Projection.inductive p in
- let bodies = Inductiveops.legacy_match_projection (snd env) ind in
- let body = bodies.(Projection.arg p) in
- let ty = Retyping.get_type_of (snd env) sigma c in
- let ((ind,u), args) = Inductiveops.find_mrectype (snd env) sigma ty in
- let body' = strip_lam_assum body in
- let u = EInstance.kind sigma u in
- let body' = CVars.subst_instance_constr u body' in
- let body' = EConstr.of_constr body' in
- substl (c :: List.rev args) body'
- with Retyping.RetypeError _ | Not_found ->
- anomaly (str"Cannot detype an unfolded primitive projection.")
- in DAst.get (detype d flags avoid env sigma c')
- else
- if print_primproj_params () then
- try
- let c = Retyping.expand_projection (snd env) sigma p c [] in
- DAst.get (detype d flags avoid env sigma c)
- with Retyping.RetypeError _ -> noparams ()
- else noparams ()
+ if print_primproj_params () then
+ try
+ let c = Retyping.expand_projection (snd env) sigma p c [] in
+ DAst.get (detype d flags avoid env sigma c)
+ with Retyping.RetypeError _ -> noparams ()
+ else noparams ()
| Evar (evk,cl) ->
let bound_to_itself_or_letin decl c =
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index 6b61b1452e..68626597fc 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -485,7 +485,11 @@ let is_gvar id c = match DAst.get c with
| GVar id' -> Id.equal id id'
| _ -> false
-let rec cases_pattern_of_glob_constr na = DAst.map (function
+let rec cases_pattern_of_glob_constr na c =
+ (* Forcing evaluation to ensure that the possible raising of
+ Not_found is not delayed *)
+ let c = DAst.force c in
+ DAst.map (function
| GVar id ->
begin match na with
| Name _ ->
@@ -498,6 +502,8 @@ let rec cases_pattern_of_glob_constr na = DAst.map (function
| GApp (c, l) ->
begin match DAst.get c with
| GRef (ConstructRef cstr,_) ->
+ let nparams = Inductiveops.inductive_nparams (fst cstr) in
+ let _,l = List.chop nparams l in
PatCstr (cstr,List.map (cases_pattern_of_glob_constr Anonymous) l,na)
| _ -> raise Not_found
end
@@ -505,7 +511,7 @@ let rec cases_pattern_of_glob_constr na = DAst.map (function
(* A canonical encoding of aliases *)
DAst.get (cases_pattern_of_glob_constr na' b)
| _ -> raise Not_found
- )
+ ) c
open Declarations
open Term
diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli
index 91a2ef9c1e..c189a3bcb2 100644
--- a/pretyping/glob_ops.mli
+++ b/pretyping/glob_ops.mli
@@ -89,6 +89,7 @@ val map_pattern : (glob_constr -> glob_constr) ->
(** Conversion from glob_constr to cases pattern, if possible
+ Evaluation is forced.
Take the current alias as parameter,
@raise Not_found if translation is impossible *)
val cases_pattern_of_glob_constr : Name.t -> 'a glob_constr_g -> 'a cases_pattern_g
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 2c4ca46343..4c02dc0f09 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -475,25 +475,6 @@ let compute_projections env (kn, i as ind) =
(* [Ind inst] is typed in context [params-wo-let] *)
ty
in
- let ci =
- let print_info =
- { ind_tags = []; cstr_tags = [|Context.Rel.to_tags ctx|]; style = LetStyle } in
- { ci_ind = ind;
- ci_npar = nparamargs;
- ci_cstr_ndecls = pkt.mind_consnrealdecls;
- ci_cstr_nargs = pkt.mind_consnrealargs;
- ci_pp_info = print_info }
- in
- let len = List.length ctx in
- let compat_body ccl i =
- (* [ccl] is defined in context [params;x:indty] *)
- (* [ccl'] is defined in context [params;x:indty;x:indty] *)
- let ccl' = liftn 1 2 ccl in
- let p = mkLambda (x, lift 1 indty, ccl') in
- let branch = it_mkLambda_or_LetIn (mkRel (len - i)) ctx in
- let body = mkCase (ci, p, mkRel 1, [|lift 1 branch|]) in
- it_mkLambda_or_LetIn (mkLambda (x,indty,body)) params
- in
let projections decl (proj_arg, j, pbs, subst) =
match decl with
| LocalDef (na,c,t) ->
@@ -523,10 +504,9 @@ let compute_projections env (kn, i as ind) =
let ty = substl subst t in
let term = mkProj (Projection.make kn true, mkRel 1) in
let fterm = mkProj (Projection.make kn false, mkRel 1) in
- let compat = compat_body ty (j - 1) in
let etab = it_mkLambda_or_LetIn (mkLambda (x, indty, term)) params in
let etat = it_mkProd_or_LetIn (mkProd (x, indty, ty)) params in
- let body = (etab, etat, compat) in
+ let body = (etab, etat) in
(proj_arg + 1, j + 1, body :: pbs, fterm :: subst)
| Anonymous ->
anomaly Pp.(str "Trying to build primitive projections for a non-primitive record")
@@ -536,13 +516,6 @@ let compute_projections env (kn, i as ind) =
in
Array.rev_of_list pbs
-let legacy_match_projection env ind =
- Array.map pi3 (compute_projections env ind)
-
-let compute_projections ind mib =
- let ans = compute_projections ind mib in
- Array.map (fun (prj, ty, _) -> (prj, ty)) ans
-
(**************************************************)
let extract_mrectype sigma t =
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index b2e205115f..5a4257e175 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -194,14 +194,6 @@ val compute_projections : Environ.env -> inductive -> (constr * types) array
(** Given a primitive record type, for every field computes the eta-expanded
projection and its type. *)
-val legacy_match_projection : Environ.env -> inductive -> constr array
-(** Given a record type, computes the legacy match-based projection of the
- projections.
-
- BEWARE: such terms are ill-typed, and should thus only be used in upper
- layers. The kernel will probably badly fail if presented with one of
- those. *)
-
(********************)
val type_of_inductive_knowing_conclusion :
diff --git a/test-suite/bugs/closed/bug_5197.v b/test-suite/bugs/closed/bug_5197.v
index b67e93d677..0c236e12ad 100644
--- a/test-suite/bugs/closed/bug_5197.v
+++ b/test-suite/bugs/closed/bug_5197.v
@@ -1,6 +1,6 @@
Set Universe Polymorphism.
Set Primitive Projections.
-Unset Printing Primitive Projection Compatibility.
+
Axiom Ω : Type.
Record Pack (A : Ω -> Type) (Aᴿ : Ω -> (forall ω : Ω, A ω) -> Type) := mkPack {
diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out
index efa895d709..5bf4ec7bfb 100644
--- a/test-suite/output/Notations4.out
+++ b/test-suite/output/Notations4.out
@@ -53,3 +53,23 @@ Notation Cn := Foo.FooCn
Expands to: Notation Notations4.J.Mfoo.Foo.Bar.Cn
let v := 0%test17 in v : myint63
: myint63
+fun y : nat => # (x, z) |-> y & y
+ : forall y : nat,
+ (?T1 * ?T2 -> ?T1 * ?T2 * nat) * (?T * ?T0 -> ?T * ?T0 * nat)
+where
+?T : [y : nat pat : ?T * ?T0 p0 : ?T * ?T0 p := p0 : ?T * ?T0
+ |- Type] (pat, p0, p cannot be used)
+?T0 : [y : nat pat : ?T * ?T0 p0 : ?T * ?T0 p := p0 : ?T * ?T0
+ |- Type] (pat, p0, p cannot be used)
+?T1 : [y : nat pat : ?T1 * ?T2 p0 : ?T1 * ?T2 p := p0 : ?T1 * ?T2
+ |- Type] (pat, p0, p cannot be used)
+?T2 : [y : nat pat : ?T1 * ?T2 p0 : ?T1 * ?T2 p := p0 : ?T1 * ?T2
+ |- Type] (pat, p0, p cannot be used)
+fun y : nat => # (x, z) |-> (x + y) & (y + z)
+ : forall y : nat,
+ (nat * ?T -> nat * ?T * nat) * (?T0 * nat -> ?T0 * nat * nat)
+where
+?T : [y : nat pat : nat * ?T p0 : nat * ?T p := p0 : nat * ?T
+ |- Type] (pat, p0, p cannot be used)
+?T0 : [y : nat pat : ?T0 * nat p0 : ?T0 * nat p := p0 : ?T0 * nat
+ |- Type] (pat, p0, p cannot be used)
diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v
index b4c65ce196..b33ad17ed4 100644
--- a/test-suite/output/Notations4.v
+++ b/test-suite/output/Notations4.v
@@ -210,3 +210,12 @@ Module NumeralNotations.
Check let v := 0%test17 in v : myint63.
End Test17.
End NumeralNotations.
+
+Module K.
+
+Notation "# x |-> t & u" := ((fun x => (x,t)),(fun x => (x,u)))
+ (at level 0, x pattern, t, u at level 39).
+Check fun y : nat => # (x,z) |-> y & y.
+Check fun y : nat => # (x,z) |-> (x + y) & (y + z).
+
+End K.
diff --git a/test-suite/success/Notations2.v b/test-suite/success/Notations2.v
index 1b33863e3b..2533a39cc4 100644
--- a/test-suite/success/Notations2.v
+++ b/test-suite/success/Notations2.v
@@ -154,3 +154,14 @@ Module M16.
Print Grammar foo.
Print Grammar foo2.
End M16.
+
+(* Example showing the need for strong evaluation of
+ cases_pattern_of_glob_constr (this used to raise Not_found at some
+ time) *)
+
+Module M17.
+
+Notation "# x ## t & u" := ((fun x => (x,t)),(fun x => (x,u))) (at level 0, x pattern).
+Check fun y : nat => # (x,z) ## y & y.
+
+End M17.
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 6c4b0acd52..d511bcd4fd 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -609,6 +609,11 @@ let vernac_assumption ~atts discharge kind l nl =
let status = ComAssumption.do_assumptions ~program_mode:atts.program kind nl l in
if not status then Feedback.feedback Feedback.AddedAxiom
+let is_polymorphic_inductive_cumulativity =
+ declare_bool_option_and_ref ~depr:false ~value:false
+ ~name:"Polymorphic inductive cumulativity"
+ ~key:["Polymorphic"; "Inductive"; "Cumulativity"]
+
let should_treat_as_cumulative cum poly =
match cum with
| Some VernacCumulative ->
@@ -617,7 +622,7 @@ let should_treat_as_cumulative cum poly =
| Some VernacNonCumulative ->
if poly then false
else user_err Pp.(str "The NonCumulative prefix can only be used in a polymorphic context.")
- | None -> poly && Flags.is_polymorphic_inductive_cumulativity ()
+ | None -> poly && is_polymorphic_inductive_cumulativity ()
let get_uniform_inductive_parameters =
Goptions.declare_bool_option_and_ref
@@ -1564,14 +1569,6 @@ let () =
optwrite = (fun b -> Flags.raw_print := b) }
let () =
- declare_bool_option
- { optdepr = false;
- optname = "Polymorphic inductive cumulativity";
- optkey = ["Polymorphic"; "Inductive"; "Cumulativity"];
- optread = Flags.is_polymorphic_inductive_cumulativity;
- optwrite = Flags.make_polymorphic_inductive_cumulativity }
-
-let () =
declare_int_option
{ optdepr = false;
optname = "the level of inlining during functor application";
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 17:04:42 +0000