aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--.gitlab-ci.yml2
-rw-r--r--dev/doc/release-process.md10
-rw-r--r--dev/tools/list-contributors.sh15
-rw-r--r--doc/changelog/08-cli-tools/13822-rm-depr-cmdline.rst4
-rw-r--r--doc/changelog/09-coqide/13810-shift-return-search-backwards.rst3
-rw-r--r--doc/sphinx/language/core/modules.rst2
-rw-r--r--ide/coqide/wg_Find.ml16
-rw-r--r--lib/cWarnings.ml6
-rw-r--r--lib/cWarnings.mli7
-rw-r--r--lib/util.ml7
-rw-r--r--lib/util.mli9
-rw-r--r--plugins/funind/g_indfun.mlg25
-rw-r--r--sysinit/coqargs.ml39
-rw-r--r--sysinit/coqargs.mli9
-rw-r--r--sysinit/coqinit.ml14
-rw-r--r--sysinit/usage.ml1
-rw-r--r--test-suite/output/Function.out0
-rw-r--r--test-suite/output/Function.v31
-rw-r--r--test-suite/output/bug_13821_native_command_line_warn.out0
-rw-r--r--test-suite/output/bug_13821_native_command_line_warn.v1
-rw-r--r--toplevel/coqtop.ml10
-rw-r--r--vernac/declaremods.ml23
-rw-r--r--vernac/vernacentries.mli1
23 files changed, 152 insertions, 83 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 754c09776e..4f58dc5aac 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -828,7 +828,7 @@ plugin:ci-coq_dpdgraph:
extends: .ci-template
plugin:ci-coqhammer:
- extends: .ci-template
+ extends: .ci-template-flambda
plugin:ci-elpi:
extends: .ci-template
diff --git a/dev/doc/release-process.md b/dev/doc/release-process.md
index 894244044a..64053a62f9 100644
--- a/dev/doc/release-process.md
+++ b/dev/doc/release-process.md
@@ -63,13 +63,9 @@ in time.
the update to the Credits chapter of the reference manual.
See also [#7058](https://github.com/coq/coq/issues/7058).
- The command that was used in the previous versions to get the list
- of contributors for this version is `git shortlog -s -n
- VX.X+alpha..master | cut -f2 | sort -k 2`. Note that the ordering is
- approximative as it will misplace people with middle names. It is
- also probably not correctly handling `Co-authored-by` info that we
- have been using more lately, so should probably be updated to
- account for this.
+ The `dev/tools/list-contributors.sh` script computes the number and
+ list of contributors between Coq revisions. Typically used with
+ `VX.X+alpha..vX.X` to check the contributors of version `VX.X`.
## On the date of the feature freeze ##
diff --git a/dev/tools/list-contributors.sh b/dev/tools/list-contributors.sh
new file mode 100644
index 0000000000..c968f2e952
--- /dev/null
+++ b/dev/tools/list-contributors.sh
@@ -0,0 +1,15 @@
+#!/usr/bin/env bash
+# For compat with OSX which has a non-gnu sed which doesn't support -z
+SED=`which gsed || which sed`
+
+if [ $# != 1 ]; then
+ error "usage: $0 rev0..rev1"
+ exit 1
+fi
+
+git shortlog -s -n --group=author --group=trailer:Co-authored-by $1 | cut -f2 | sort -k 2 | grep -v -e "coqbot" -e "^$" > contributors.tmp
+
+cat contributors.tmp | wc -l | xargs echo "Contributors:"
+cat contributors.tmp | gsed -z "s/\n/, /g"
+echo
+rm contributors.tmp
diff --git a/doc/changelog/08-cli-tools/13822-rm-depr-cmdline.rst b/doc/changelog/08-cli-tools/13822-rm-depr-cmdline.rst
new file mode 100644
index 0000000000..e3333f8a9a
--- /dev/null
+++ b/doc/changelog/08-cli-tools/13822-rm-depr-cmdline.rst
@@ -0,0 +1,4 @@
+- **Removed:** previously deprecated command line options
+ ``-sprop-cumulative`` and ``-input-state`` and its alias ``-is``
+ (`#13822 <https://github.com/coq/coq/pull/13822>`_,
+ by Gaëtan Gilbert).
diff --git a/doc/changelog/09-coqide/13810-shift-return-search-backwards.rst b/doc/changelog/09-coqide/13810-shift-return-search-backwards.rst
new file mode 100644
index 0000000000..e78280d91d
--- /dev/null
+++ b/doc/changelog/09-coqide/13810-shift-return-search-backwards.rst
@@ -0,0 +1,3 @@
+- **Added:**
+ Shift-return in the Find dialog now searches backwards (`#13810 <https://github.com/coq/coq/pull/13810>`_,
+ by slrnsc).
diff --git a/doc/sphinx/language/core/modules.rst b/doc/sphinx/language/core/modules.rst
index 93d70c773f..4ea9606c18 100644
--- a/doc/sphinx/language/core/modules.rst
+++ b/doc/sphinx/language/core/modules.rst
@@ -880,7 +880,7 @@ started, unless option ``-top`` or ``-notop`` is set (see :ref:`command-line-opt
.. _qualified-names:
Qualified identifiers
----------------------
+~~~~~~~~~~~~~~~~~~~~~
.. insertprodn qualid field_ident
diff --git a/ide/coqide/wg_Find.ml b/ide/coqide/wg_Find.ml
index 7e89191bd1..7f30cc8c6c 100644
--- a/ide/coqide/wg_Find.ml
+++ b/ide/coqide/wg_Find.ml
@@ -219,16 +219,18 @@ class finder name (view : GText.view) =
let _ = replace_all_button#connect#clicked ~callback:self#replace_all in
(* Keypress interaction *)
- let generic_cb esc_cb ret_cb ev =
+ let dispatch_key_cb esc_cb ret_cb shift_ret_cb ev =
let ev_key = GdkEvent.Key.keyval ev in
- let (return, _) = GtkData.AccelGroup.parse "Return" in
- let (esc, _) = GtkData.AccelGroup.parse "Escape" in
- if ev_key = return then (ret_cb (); true)
- else if ev_key = esc then (esc_cb (); true)
+ let ev_modifiers = GdkEvent.Key.state ev in
+ if ev_key = GdkKeysyms._Return then
+ (if List.mem `SHIFT ev_modifiers then
+ shift_ret_cb ()
+ else ret_cb (); true)
+ else if ev_key = GdkKeysyms._Escape then (esc_cb (); true)
else false
in
- let find_cb = generic_cb self#hide self#find_forward in
- let replace_cb = generic_cb self#hide self#replace in
+ let find_cb = dispatch_key_cb self#hide self#find_forward self#find_backward in
+ let replace_cb = dispatch_key_cb self#hide self#replace self#replace in
let _ = find_entry#event#connect#key_press ~callback:find_cb in
let _ = replace_entry#event#connect#key_press ~callback:replace_cb in
diff --git a/lib/cWarnings.ml b/lib/cWarnings.ml
index cc1fa647f9..ee7dab92bc 100644
--- a/lib/cWarnings.ml
+++ b/lib/cWarnings.ml
@@ -173,3 +173,9 @@ let create ~name ~category ?(default=Enabled) pp =
| Disabled -> ()
| AsError -> CErrors.user_err ?loc (pp x)
| Enabled -> Feedback.msg_warning ?loc (pp x)
+
+(* Remark: [warn] does not need to start with a comma, but if present
+ it won't hurt (",," is normalized into ","). *)
+let with_warn warn (f:'b -> 'a) x =
+ let s = get_flags () in
+ Util.try_finally (fun x -> set_flags (s^","^warn);f x) x set_flags s
diff --git a/lib/cWarnings.mli b/lib/cWarnings.mli
index ded1f9be3b..b63eed09d0 100644
--- a/lib/cWarnings.mli
+++ b/lib/cWarnings.mli
@@ -19,3 +19,10 @@ val set_flags : string -> unit
(** Cleans up a user provided warnings status string, e.g. removing unknown
warnings (in which case a warning is emitted) or subsumed warnings . *)
val normalize_flags_string : string -> string
+
+(** [with_warn "-xxx,+yyy..." f x] calls [f x] after setting the
+ warnings as specified in the string (keeping other previously set
+ warnings), and restores current warnings after [f()] returns or
+ raises an exception. If both f and restoring the warnings raise
+ exceptions, the latter is raised. *)
+val with_warn: string -> ('b -> 'a) -> 'b -> 'a
diff --git a/lib/util.ml b/lib/util.ml
index 87cc30e557..e8aa0f3e48 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -135,6 +135,13 @@ type 'a delayed = unit -> 'a
let delayed_force f = f ()
+(* finalize - Credit X.Leroy, D.Remy. *)
+let try_finally f x finally y =
+ let res = try f x with exn -> finally y; raise exn in
+ finally y;
+ res
+
+
(* Misc *)
type ('a, 'b) union = ('a, 'b) CSig.union = Inl of 'a | Inr of 'b
diff --git a/lib/util.mli b/lib/util.mli
index fe34525671..aefb015c38 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -112,6 +112,15 @@ type 'a delayed = unit -> 'a
val delayed_force : 'a delayed -> 'a
+(** [try_finally f x g y] applies the main code [f] to [x] and
+ returns the result after having applied the finalization
+ code [g] to [y]. If the main code raises the exception
+ [exn], the finalization code is executed and [exn] is raised.
+ If the finalization code itself fails, the exception
+ returned is always the one from the finalization code.
+ Credit X.Leroy, D.Remy. *)
+val try_finally: ('a -> 'b) -> 'a -> ('c -> unit) -> 'c -> 'b
+
(** {6 Enriched exceptions} *)
type iexn = Exninfo.iexn
diff --git a/plugins/funind/g_indfun.mlg b/plugins/funind/g_indfun.mlg
index ca6ae150a7..15cf88f827 100644
--- a/plugins/funind/g_indfun.mlg
+++ b/plugins/funind/g_indfun.mlg
@@ -195,16 +195,29 @@ let is_interactive recsl =
}
+(* For usability we temporarily switch off some flags during the call
+ to Function. However this is not satisfactory:
+
+ 1- Function should not warn "non-recursive" and call the Definition
+ mechanism instead of Fixpoint when needed
+
+ 2- Only for automatically generated names should
+ unused-pattern-matching-variable be ignored. *)
+
VERNAC COMMAND EXTEND Function STATE CUSTOM
| ["Function" ne_function_fix_definition_list_sep(recsl,"with")]
=> { classify_funind recsl }
-> {
- if is_interactive recsl then
- Vernacextend.VtOpenProof (fun () ->
- Gen_principle.do_generate_principle_interactive (List.map snd recsl))
- else
- Vernacextend.VtDefault (fun () ->
- Gen_principle.do_generate_principle (List.map snd recsl)) }
+ let warn = "-unused-pattern-matching-variable,-matching-variable,-non-recursive" in
+ if is_interactive recsl then
+ Vernacextend.VtOpenProof (fun () ->
+ CWarnings.with_warn warn
+ Gen_principle.do_generate_principle_interactive (List.map snd recsl))
+ else
+ Vernacextend.VtDefault (fun () ->
+ CWarnings.with_warn warn
+ Gen_principle.do_generate_principle (List.map snd recsl))
+ }
END
{
diff --git a/sysinit/coqargs.ml b/sysinit/coqargs.ml
index c4f12f6bb7..56d88e6bd6 100644
--- a/sysinit/coqargs.ml
+++ b/sysinit/coqargs.ml
@@ -44,6 +44,7 @@ type option_command =
type injection_command =
| OptionInjection of (Goptions.option_name * option_command)
| RequireInjection of (string * string option * bool option)
+ | WarnNoNative of string
type coqargs_logic_config = {
impredicative_set : Declarations.set_predicativity;
@@ -75,8 +76,6 @@ type coqargs_pre = {
load_vernacular_list : (string * bool) list;
injections : injection_command list;
-
- inputstate : string option;
}
type coqargs_query =
@@ -133,7 +132,6 @@ let default_pre = {
vo_includes = [];
load_vernacular_list = [];
injections = [];
- inputstate = None;
}
let default_queries = []
@@ -184,18 +182,6 @@ let set_query opts q =
| Queries queries -> Queries (queries@[q])
}
-let warn_deprecated_sprop_cumul =
- CWarnings.create ~name:"deprecated-spropcumul" ~category:"deprecated"
- (fun () -> Pp.strbrk "Use the \"Cumulative StrictProp\" flag instead.")
-
-let warn_deprecated_inputstate =
- CWarnings.create ~name:"deprecated-inputstate" ~category:"deprecated"
- (fun () -> Pp.strbrk "The inputstate option is deprecated and discouraged.")
-
-let set_inputstate opts s =
- warn_deprecated_inputstate ();
- { opts with pre = { opts.pre with inputstate = Some s }}
-
(******************************************************************************)
(* Parsing helpers *)
(******************************************************************************)
@@ -255,12 +241,6 @@ let parse_option_set opt =
let v = String.sub opt (eqi+1) (len - eqi - 1) in
to_opt_key (String.sub opt 0 eqi), Some v
-let warn_no_native_compiler =
- CWarnings.create ~name:"native-compiler-disabled" ~category:"native-compiler"
- Pp.(fun s -> strbrk "Native compiler is disabled," ++
- strbrk " -native-compiler " ++ strbrk s ++
- strbrk " option ignored.")
-
let get_native_compiler s =
(* We use two boolean flags because the four states make sense, even if
only three are accessible to the user at the moment. The selection of the
@@ -274,10 +254,8 @@ let get_native_compiler s =
| _ ->
error_wrong_arg ("Error: (yes|no|ondemand) expected after option -native-compiler") in
if Coq_config.native_compiler = NativeOff && n <> NativeOff then
- let () = warn_no_native_compiler s in
- NativeOff
- else
- n
+ NativeOff, Some (WarnNoNative s)
+ else n, None
(* Main parsing routine *)
(*s Parsing of the command line *)
@@ -333,9 +311,6 @@ let parse_args ~usage ~init arglist : t * string list =
|"-init-file" ->
{ oval with config = { oval.config with rcfile = Some (next ()); }}
- |"-inputstate"|"-is" ->
- set_inputstate oval (next ())
-
|"-load-vernac-object" ->
add_vo_require oval (next ()) None None
@@ -385,8 +360,9 @@ let parse_args ~usage ~init arglist : t * string list =
{ oval with config = { oval.config with enable_VM = get_bool ~opt (next ()) }}
|"-native-compiler" ->
- let native_compiler = get_native_compiler (next ()) in
- { oval with config = { oval.config with native_compiler }}
+ let native_compiler, warn = get_native_compiler (next ()) in
+ { oval with config = { oval.config with native_compiler };
+ pre = { oval.pre with injections = Option.List.cons warn oval.pre.injections }}
| "-set" ->
let opt, v = parse_option_set @@ next() in
@@ -419,9 +395,6 @@ let parse_args ~usage ~init arglist : t * string list =
add_set_option oval Vernacentries.allow_sprop_opt_name (OptionSet None)
|"-disallow-sprop" ->
add_set_option oval Vernacentries.allow_sprop_opt_name OptionUnset
- |"-sprop-cumulative" ->
- warn_deprecated_sprop_cumul();
- add_set_option oval Vernacentries.cumul_sprop_opt_name (OptionSet None)
|"-indices-matter" -> set_logic (fun o -> { o with indices_matter = true }) oval
|"-m"|"--memory" -> { oval with post = { memory_stat = true }}
|"-noinit"|"-nois" -> { oval with pre = { oval.pre with load_init = false }}
diff --git a/sysinit/coqargs.mli b/sysinit/coqargs.mli
index aef50193f2..9725a849a4 100644
--- a/sysinit/coqargs.mli
+++ b/sysinit/coqargs.mli
@@ -28,7 +28,12 @@ type injection_command =
ready. Parameters follow [Library], that is to say,
[lib,prefix,import_export] means require library [lib] from
optional [prefix] and [import_export] if [Some false/Some true]
- is used. *)
+ is used. *)
+ | WarnNoNative of string
+ (** Used so that "-w -native-compiler-disabled -native-compiler yes"
+ does not cause a warning. The native option must be processed
+ before injections (because it affects require), so the
+ instruction to emit a message is separated. *)
type coqargs_logic_config = {
impredicative_set : Declarations.set_predicativity;
@@ -60,8 +65,6 @@ type coqargs_pre = {
load_vernacular_list : (string * bool) list;
injections : injection_command list;
-
- inputstate : string option;
}
type coqargs_query =
diff --git a/sysinit/coqinit.ml b/sysinit/coqinit.ml
index 16c8389de5..25da2c5302 100644
--- a/sysinit/coqinit.ml
+++ b/sysinit/coqinit.ml
@@ -126,10 +126,16 @@ let require_file (dir, from, exp) =
let mfrom = Option.map Libnames.qualid_of_string from in
Flags.silently (Vernacentries.vernac_require mfrom exp) [mp]
-let handle_injection = function
- | Coqargs.RequireInjection r -> require_file r
- (* | LoadInjection l -> *)
- | Coqargs.OptionInjection o -> Coqargs.set_option o
+let warn_no_native_compiler =
+ CWarnings.create ~name:"native-compiler-disabled" ~category:"native-compiler"
+ Pp.(fun s -> strbrk "Native compiler is disabled," ++
+ strbrk " -native-compiler " ++ strbrk s ++
+ strbrk " option ignored.")
+
+let handle_injection = let open Coqargs in function
+ | RequireInjection r -> require_file r
+ | OptionInjection o -> set_option o
+ | WarnNoNative s -> warn_no_native_compiler s
let start_library ~top injections =
Flags.verbosely Declaremods.start_library top;
diff --git a/sysinit/usage.ml b/sysinit/usage.ml
index 1831a3f9b2..763cd54137 100644
--- a/sysinit/usage.ml
+++ b/sysinit/usage.ml
@@ -79,7 +79,6 @@ let print_usage_common co command =
\n -impredicative-set set sort Set impredicative\
\n -allow-sprop allow using the proof irrelevant SProp sort\
\n -disallow-sprop forbid using the proof irrelevant SProp sort\
-\n -sprop-cumulative make sort SProp cumulative with the rest of the hierarchy\
\n -indices-matter levels of indices (and nonuniform parameters) contribute to the level of inductives\
\n -type-in-type disable universe consistency checking\
\n -mangle-names x mangle auto-generated names using prefix x\
diff --git a/test-suite/output/Function.out b/test-suite/output/Function.out
new file mode 100644
index 0000000000..e69de29bb2
--- /dev/null
+++ b/test-suite/output/Function.out
diff --git a/test-suite/output/Function.v b/test-suite/output/Function.v
new file mode 100644
index 0000000000..b3e2a93895
--- /dev/null
+++ b/test-suite/output/Function.v
@@ -0,0 +1,31 @@
+Require Import FunInd List.
+
+(* Explanations: This kind of pattern matching displays a legitimate
+ unused variable warning in v8.13.
+
+Fixpoint f (l:list nat) : nat :=
+ match l with
+ | nil => O
+ | S n :: nil => 1
+ | x :: l' => f l'
+ end.
+*)
+
+(* In v8.13 the same code with "Function" generates a lot more
+ warnings about variables created automatically by Function. These
+ are not legitimate. PR #13776 (post v8.13) removes all warnings
+ about pattern matching variables (and non truly recursive fixpoint)
+ for "Function". So this should not generate any warning. Note that
+ this PR removes also the legitimate warnings. It would be better if
+ this test generate the same warning as the Fixpoint above. This
+ test would then need to be updated. *)
+
+(* Ensuring the warning is a warning. *)
+Set Warnings "matching-variable".
+(* But no warning generated here. *)
+Function f (l:list nat) : nat :=
+ match l with
+ | nil => O
+ | S n :: nil => 1
+ | n :: l' => f l'
+ end.
diff --git a/test-suite/output/bug_13821_native_command_line_warn.out b/test-suite/output/bug_13821_native_command_line_warn.out
new file mode 100644
index 0000000000..e69de29bb2
--- /dev/null
+++ b/test-suite/output/bug_13821_native_command_line_warn.out
diff --git a/test-suite/output/bug_13821_native_command_line_warn.v b/test-suite/output/bug_13821_native_command_line_warn.v
new file mode 100644
index 0000000000..a28210b6c2
--- /dev/null
+++ b/test-suite/output/bug_13821_native_command_line_warn.v
@@ -0,0 +1 @@
+(* -*- coq-prog-args: ("-w" "-native-compiler-disabled" "-native-compiler" "ondemand"); -*- *)
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index caf86ef870..16028be910 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -35,14 +35,6 @@ let print_header () =
(******************************************************************************)
-(* Input/Output State *)
-(******************************************************************************)
-let inputstate opts =
- Option.iter (fun istate_file ->
- let fname = Loadpath.locate_file (CUnix.make_suffix istate_file ".coq") in
- Vernacstate.System.load fname) opts.inputstate
-
-(******************************************************************************)
(* Fatal Errors *)
(******************************************************************************)
@@ -70,8 +62,6 @@ let init_toplevel { parse_extra; init_extra; usage; initial_args } =
let opts, customopts = Coqinit.parse_arguments ~parse_extra ~usage ~initial_args () in
Stm.init_process (snd customopts);
let injections = Coqinit.init_runtime opts in
- (* Allow the user to load an arbitrary state here *)
- inputstate opts.pre;
(* This state will be shared by all the documents *)
Stm.init_core ();
let customstate = init_extra ~opts customopts injections in
diff --git a/vernac/declaremods.ml b/vernac/declaremods.ml
index d2eeebc246..15e6d4ef37 100644
--- a/vernac/declaremods.ml
+++ b/vernac/declaremods.ml
@@ -301,7 +301,10 @@ and load_keep i ((sp,kn),kobjs) =
let mark_object f obj (exports,acc) =
(exports, (f,obj)::acc)
-let rec collect_module_objects (f,mp) acc =
+let rec collect_modules mpl acc =
+ List.fold_left (fun acc fmp -> collect_module fmp acc) acc (List.rev mpl)
+
+and collect_module (f,mp) acc =
(* May raise Not_found for unknown module and for functors *)
let modobjs = ModObjs.get mp in
let prefix = modobjs.module_prefix in
@@ -310,14 +313,16 @@ let rec collect_module_objects (f,mp) acc =
and collect_object f i (name, obj as o) acc =
match obj with
- | ExportObject { mpl } -> collect_export f i mpl acc
+ | ExportObject { mpl } -> collect_exports f i mpl acc
| AtomicObject _ | IncludeObject _ | KeepObject _
| ModuleObject _ | ModuleTypeObject _ -> mark_object f o acc
and collect_objects f i prefix objs acc =
- List.fold_right (fun (id, obj) acc -> collect_object f i (Lib.make_oname prefix id, obj) acc) objs acc
+ List.fold_left (fun acc (id, obj) ->
+ collect_object f i (Lib.make_oname prefix id, obj) acc
+ ) acc (List.rev objs)
-and collect_one_export f (f',mp) (exports,objs as acc) =
+and collect_export f (f',mp) (exports,objs as acc) =
match filter_and f f' with
| None -> acc
| Some f ->
@@ -334,12 +339,12 @@ and collect_one_export f (f',mp) (exports,objs as acc) =
*)
if exports == exports' then acc
else
- collect_module_objects (f,mp) (exports', objs)
+ collect_module (f,mp) (exports', objs)
-and collect_export f i mpl acc =
+and collect_exports f i mpl acc =
if Int.equal i 1 then
- List.fold_right (collect_one_export f) mpl acc
+ List.fold_left (fun acc fmp -> collect_export f fmp acc) acc (List.rev mpl)
else acc
let open_modtype i ((sp,kn),_) =
@@ -388,7 +393,7 @@ and open_include f i ((sp,kn), aobjs) =
open_objects f i prefix o
and open_export f i mpl =
- let _,objs = collect_export f i mpl (MPmap.empty, []) in
+ let _,objs = collect_exports f i mpl (MPmap.empty, []) in
List.iter (fun (f,o) -> open_object f 1 o) objs
and open_keep f i ((sp,kn),kobjs) =
@@ -1056,7 +1061,7 @@ let end_library ?except ~output_native_objects dir =
cenv,(substitute,keep),ast
let import_modules ~export mpl =
- let _,objs = List.fold_right collect_module_objects mpl (MPmap.empty, []) in
+ let _,objs = collect_modules mpl (MPmap.empty, []) in
List.iter (fun (f,o) -> open_object f 1 o) objs;
if export then Lib.add_anonymous_entry (Lib.Leaf (ExportObject { mpl }))
diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli
index cf233248d7..2ac8458ad5 100644
--- a/vernac/vernacentries.mli
+++ b/vernac/vernacentries.mli
@@ -26,4 +26,3 @@ val interp_redexp_hook : (Environ.env -> Evd.evar_map -> Genredexpr.raw_red_expr
val command_focus : unit Proof.focus_kind
val allow_sprop_opt_name : string list
-val cumul_sprop_opt_name : string list
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 23:10:26 +0000