aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rwxr-xr-xdev/tools/update-compat.py62
-rw-r--r--doc/sphinx/proof-engine/tactics.rst10
-rw-r--r--kernel/reduction.ml10
-rw-r--r--kernel/retypeops.ml30
-rw-r--r--kernel/retypeops.mli4
-rw-r--r--plugins/ssr/ssrbool.v2
-rw-r--r--pretyping/retyping.ml13
-rw-r--r--test-suite/output/Arguments.out14
-rw-r--r--test-suite/output/Arguments_renaming.out24
-rw-r--r--test-suite/output/Cases.out4
-rw-r--r--test-suite/output/Implicit.out2
-rw-r--r--test-suite/output/InitSyntax.out4
-rw-r--r--test-suite/output/PatternsInBinders.out2
-rw-r--r--test-suite/output/PrintInfos.out24
-rw-r--r--test-suite/output/UnivBinders.out2
-rw-r--r--vernac/comArguments.ml19
-rw-r--r--vernac/comArguments.mli2
-rw-r--r--vernac/g_vernac.mlg31
-rw-r--r--vernac/ppvernac.ml53
-rw-r--r--vernac/prettyp.ml26
-rw-r--r--vernac/vernacentries.ml4
-rw-r--r--vernac/vernacexpr.ml8
22 files changed, 196 insertions, 154 deletions
diff --git a/dev/tools/update-compat.py b/dev/tools/update-compat.py
index c7bb36b6d3..7312c2a5af 100755
--- a/dev/tools/update-compat.py
+++ b/dev/tools/update-compat.py
@@ -1,6 +1,8 @@
-#!/usr/bin/env python2
+#!/usr/bin/env python3
from __future__ import with_statement
+from __future__ import print_function
import os, re, sys, subprocess
+from io import open
# When passed `--release`, this script sets up Coq to support three
# `-compat` flag arguments. If executed manually, this would consist
@@ -84,17 +86,25 @@ BUG_HEADER = r"""(* DO NOT MODIFY THIS FILE DIRECTLY *)
(* It is autogenerated by %s. *)
""" % os.path.relpath(os.path.realpath(__file__), ROOT_PATH)
+def get_file_lines(file_name):
+ with open(file_name, 'rb') as f:
+ lines = f.readlines()
+ return [line.decode('utf-8') for line in lines]
+
+def get_file(file_name):
+ return ''.join(get_file_lines(file_name))
+
def get_header():
- with open(HEADER_PATH, 'r') as f: return f.read()
+ return get_file(HEADER_PATH)
HEADER = get_header()
-def break_or_continue():
- msg = 'Press ENTER to continue, or Ctrl+C to break...'
- try:
- raw_input(msg)
- except NameError: # we must be running python3
- input(msg)
+def fatal_error(msg):
+ if hasattr(sys.stderr, 'buffer'):
+ sys.stderr.buffer.write(msg.encode("utf-8"))
+ else:
+ sys.stderr.write(msg.encode("utf-8"))
+ sys.exit(1)
def maybe_git_add(local_path, suggest_add=True, **args):
if args['git_add']:
@@ -114,11 +124,10 @@ def maybe_git_rm(local_path, **args):
def get_version(cur_version=None):
if cur_version is not None: return cur_version
- with open(CONFIGURE_PATH, 'r') as f:
- for line in f.readlines():
- found = re.findall(r'let coq_version = "([0-9]+\.[0-9]+)', line)
- if len(found) > 0:
- return found[0]
+ for line in get_file_lines(CONFIGURE_PATH):
+ found = re.findall(r'let coq_version = "([0-9]+\.[0-9]+)', line)
+ if len(found) > 0:
+ return found[0]
raise Exception("No line 'let coq_version = \"X.X' found in %s" % os.path.relpath(CONFIGURE_PATH, ROOT_PATH))
def compat_name_to_version_name(compat_file_name):
@@ -132,8 +141,7 @@ def version_name_to_compat_name(v, ext='.v'):
# returns (lines of compat files, lines of not compat files
def get_doc_index_lines():
- with open(DOC_INDEX_PATH, 'r') as f:
- lines = f.readlines()
+ lines = get_file_lines(DOC_INDEX_PATH)
return (tuple(line for line in lines if 'theories/Compat/Coq' in line),
tuple(line for line in lines if 'theories/Compat/Coq' not in line))
@@ -183,7 +191,7 @@ def update_if_changed(contents, new_contents, path, exn_string='%s changed!', su
if contents is None or contents != new_contents:
if not assert_unchanged:
print('Updating %s...' % os.path.relpath(path, ROOT_PATH))
- with open(path, 'w') as f:
+ with open(path, 'w', encoding='utf-8') as f:
f.write(new_contents)
maybe_git_add(os.path.relpath(path, ROOT_PATH), suggest_add=suggest_add, **args)
else:
@@ -226,8 +234,7 @@ def update_compat_files(old_versions, new_versions, assert_unchanged=False, **ar
update_file(contents, compat_path, exn_string='%s does not exist!', assert_unchanged=assert_unchanged, **args)
else:
# print('Checking %s...' % compat_file)
- with open(compat_path, 'r') as f:
- contents = f.read()
+ contents = get_file(compat_path)
header = HEADER + (EXTRA_HEADER % v)
if not contents.startswith(HEADER):
raise Exception("Invalid header in %s; does not match %s" % (compat_file, os.path.relpath(HEADER_PATH, ROOT_PATH)))
@@ -323,13 +330,13 @@ def check_no_old_versions(old_versions, new_versions, contents, relpath):
raise Exception('Unreplaced usage of %s remaining in %s' % (V, relpath))
def update_flags_mli(old_versions, new_versions, **args):
- with open(FLAGS_MLI_PATH, 'r') as f: contents = f.read()
+ contents = get_file(FLAGS_MLI_PATH)
new_contents = update_compat_versions_type_line(new_versions, contents, os.path.relpath(FLAGS_MLI_PATH, ROOT_PATH))
check_no_old_versions(old_versions, new_versions, new_contents, os.path.relpath(FLAGS_MLI_PATH, ROOT_PATH))
update_if_changed(contents, new_contents, FLAGS_MLI_PATH, **args)
def update_flags_ml(old_versions, new_versions, **args):
- with open(FLAGS_ML_PATH, 'r') as f: contents = f.read()
+ contents = get_file(FLAGS_ML_PATH)
new_contents = update_compat_versions_type_line(new_versions, contents, os.path.relpath(FLAGS_ML_PATH, ROOT_PATH))
new_contents = update_version_compare(new_versions, new_contents, os.path.relpath(FLAGS_ML_PATH, ROOT_PATH))
new_contents = update_pr_version(new_versions, new_contents, os.path.relpath(FLAGS_ML_PATH, ROOT_PATH))
@@ -337,13 +344,13 @@ def update_flags_ml(old_versions, new_versions, **args):
update_if_changed(contents, new_contents, FLAGS_ML_PATH, **args)
def update_coqargs_ml(old_versions, new_versions, **args):
- with open(COQARGS_ML_PATH, 'r') as f: contents = f.read()
+ contents = get_file(COQARGS_ML_PATH)
new_contents = update_add_compat_require(new_versions, contents, os.path.relpath(COQARGS_ML_PATH, ROOT_PATH))
check_no_old_versions(old_versions, new_versions, new_contents, os.path.relpath(COQARGS_ML_PATH, ROOT_PATH))
update_if_changed(contents, new_contents, COQARGS_ML_PATH, **args)
def update_g_vernac(old_versions, new_versions, **args):
- with open(G_VERNAC_PATH, 'r') as f: contents = f.read()
+ contents = get_file(G_VERNAC_PATH)
new_contents = update_parse_compat_version(new_versions, contents, os.path.relpath(G_VERNAC_PATH, ROOT_PATH), **args)
check_no_old_versions(old_versions, new_versions, new_contents, os.path.relpath(G_VERNAC_PATH, ROOT_PATH))
update_if_changed(contents, new_contents, G_VERNAC_PATH, **args)
@@ -361,7 +368,7 @@ def update_test_suite(new_versions, assert_unchanged=False, test_suite_paths=TES
contents = None
suggest_add = False
if os.path.exists(path):
- with open(path, 'r') as f: contents = f.read()
+ contents = get_file(path)
else:
suggest_add = True
if '%s' in descr: descr = descr % v
@@ -376,7 +383,7 @@ def update_test_suite(new_versions, assert_unchanged=False, test_suite_paths=TES
remove_if_exists(path, assert_unchanged=assert_unchanged, **args)
def update_doc_index(new_versions, **args):
- with open(DOC_INDEX_PATH, 'r') as f: contents = f.read()
+ contents = get_file(DOC_INDEX_PATH)
firstline = ' theories/Compat/AdmitAxiom.v'
new_contents = ''.join(DOC_INDEX_LINES)
if firstline not in new_contents:
@@ -386,7 +393,7 @@ def update_doc_index(new_versions, **args):
update_if_changed(contents, new_contents, DOC_INDEX_PATH, **args)
def update_test_suite_run(**args):
- with open(TEST_SUITE_RUN_PATH, 'r') as f: contents = f.read()
+ contents = get_file(TEST_SUITE_RUN_PATH)
new_contents = r'''#!/usr/bin/env bash
# allow running this script from any directory by basing things on where the script lives
@@ -410,7 +417,7 @@ def update_compat_notations(old_versions, new_versions, **args):
for root, dirs, files in os.walk(os.path.join(ROOT_PATH, 'theories')):
for fname in files:
if not fname.endswith('.v'): continue
- with open(os.path.join(root, fname), 'r') as f: contents = f.read()
+ contents = get_file(os.path.join(root, fname))
new_contents = update_compat_notations_in(old_versions, new_versions, contents)
update_if_changed(contents, new_contents, os.path.join(root, fname), **args)
@@ -435,9 +442,8 @@ def parse_args(argv):
'git_add': False,
}
if '--master' not in argv and '--release' not in argv:
- print(r'''WARNING: You should pass either --release (sometime before branching)
+ fatal_error(r'''ERROR: You should pass either --release (sometime before branching)
or --master (right after branching and updating the version number in version.ml)''')
- if '--assert-unchanged' not in args: break_or_continue()
for arg in argv[1:]:
if arg == '--assert-unchanged':
args['assert_unchanged'] = True
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 62d4aa704f..4f903d5776 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -3281,11 +3281,13 @@ the conversion in hypotheses :n:`{+ @ident}`.
defined transparent constant or local definition (see
:ref:`gallina-definitions` and
:ref:`vernac-controlling-the-reduction-strategies`). The tactic
- :tacn:`unfold` applies the :math:`\delta` rule to each occurrence of
- the constant to which :n:`@qualid` refers in the current goal and
- then replaces it with its :math:`\beta`:math:`\iota`-normal form.
+ :tacn:`unfold` applies the :math:`\delta` rule to each occurrence
+ of the constant to which :n:`@qualid` refers in the current goal
+ and then replaces it with its :math:`\beta\iota\zeta`-normal form.
+ Use the general reduction tactics if you want to avoid this final
+ reduction, for instance :n:`cbv delta [@qualid]`.
- .. exn:: @qualid does not denote an evaluable constant.
+ .. exn:: Cannot coerce @qualid to an evaluable reference.
This error is frequent when trying to unfold something that has
defined as an inductive type (or constructor) and not as a
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index f2cb9a8aec..b7bd4eef9a 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -302,7 +302,7 @@ let unfold_ref_with_args infos tab fl v =
type conv_tab = {
cnv_inf : clos_infos;
- relevances : Sorts.relevance list;
+ relevances : Sorts.relevance Range.t;
lft_tab : clos_tab;
rgt_tab : clos_tab;
}
@@ -313,16 +313,16 @@ type conv_tab = {
passed to each respective side of the conversion function below. *)
let push_relevance infos r =
- { infos with relevances = r.Context.binder_relevance :: infos.relevances }
+ { infos with relevances = Range.cons r.Context.binder_relevance infos.relevances }
let push_relevances infos nas =
- { infos with relevances = Array.fold_left (fun l x -> x.Context.binder_relevance :: l) infos.relevances nas }
+ { infos with relevances = Array.fold_left (fun l x -> Range.cons x.Context.binder_relevance l) infos.relevances nas }
let rec skip_pattern infos relevances n c1 c2 =
if Int.equal n 0 then {infos with relevances}, c1, c2
else match kind c1, kind c2 with
| Lambda (x, _, c1), Lambda (_, _, c2) ->
- skip_pattern infos (x.Context.binder_relevance :: relevances) (pred n) c1 c2
+ skip_pattern infos (Range.cons x.Context.binder_relevance relevances) (pred n) c1 c2
| _ -> raise IrregularPatternShape
let skip_pattern infos n c1 c2 =
@@ -705,7 +705,7 @@ let clos_gen_conv trans cv_pb l2r evars env univs t1 t2 =
let infos = create_clos_infos ~evars reds env in
let infos = {
cnv_inf = infos;
- relevances = List.map Context.Rel.Declaration.get_relevance (rel_context env);
+ relevances = Range.empty;
lft_tab = create_tab ();
rgt_tab = create_tab ();
} in
diff --git a/kernel/retypeops.ml b/kernel/retypeops.ml
index 5c15257511..6a1b36ea94 100644
--- a/kernel/retypeops.ml
+++ b/kernel/retypeops.ml
@@ -39,16 +39,10 @@ let relevance_of_projection env p =
let mib = lookup_mind mind env in
Declareops.relevance_of_projection_repr mib (Projection.repr p)
-let rec relevance_of_rel_extra env extra n =
- match extra with
- | [] -> relevance_of_rel env n
- | r :: _ when Int.equal n 1 -> r
- | _ :: extra -> relevance_of_rel_extra env extra (n-1)
-
-let relevance_of_flex env extra lft = function
+let relevance_of_flex env = function
| ConstKey (c,_) -> relevance_of_constant env c
| VarKey x -> relevance_of_var env x
- | RelKey p -> relevance_of_rel_extra env extra (Esubst.reloc_rel p lft)
+ | RelKey p -> relevance_of_rel env p
let rec relevance_of_fterm env extra lft f =
let open CClosure in
@@ -57,9 +51,9 @@ let rec relevance_of_fterm env extra lft f =
| KnownI -> Sorts.Irrelevant
| Unknown ->
let r = match fterm_of f with
- | FRel n -> relevance_of_rel_extra env extra (Esubst.reloc_rel n lft)
+ | FRel n -> Range.get extra (Esubst.reloc_rel n lft - 1)
| FAtom c -> relevance_of_term_extra env extra lft (Esubst.subs_id 0) c
- | FFlex key -> relevance_of_flex env extra lft key
+ | FFlex key -> relevance_of_flex env key
| FInt _ | FFloat _ -> Sorts.Relevant
| FInd _ | FProd _ -> Sorts.Relevant (* types are always relevant *)
| FConstruct (c,_) -> relevance_of_constructor env c
@@ -69,12 +63,12 @@ let rec relevance_of_fterm env extra lft f =
| FCoFix ((i,(lna,_,_)), _) -> (lna.(i)).binder_relevance
| FCaseT (ci, _, _, _, _) -> ci.ci_relevance
| FLambda (len, tys, bdy, e) ->
- let extra = List.rev_append (List.map (fun (x,_) -> binder_relevance x) tys) extra in
+ let extra = List.fold_left (fun accu (x, _) -> Range.cons (binder_relevance x) accu) extra tys in
let lft = Esubst.el_liftn len lft in
let e = Esubst.subs_liftn len e in
relevance_of_term_extra env extra lft e bdy
| FLetIn (x, _, _, bdy, e) ->
- relevance_of_term_extra env (x.binder_relevance :: extra)
+ relevance_of_term_extra env (Range.cons x.binder_relevance extra)
(Esubst.el_lift lft) (Esubst.subs_lift e) bdy
| FLIFT (k, f) -> relevance_of_fterm env extra (Esubst.el_shft k lft) f
| FCLOS (c, e) -> relevance_of_term_extra env extra lft e c
@@ -88,16 +82,18 @@ let rec relevance_of_fterm env extra lft f =
and relevance_of_term_extra env extra lft subs c =
match kind c with
| Rel n ->
- (match Esubst.expand_rel n subs with
+ begin match Esubst.expand_rel n subs with
| Inl (k, f) -> relevance_of_fterm env extra (Esubst.el_liftn k lft) f
- | Inr (n, _) -> relevance_of_rel_extra env extra (Esubst.reloc_rel n lft))
+ | Inr (n, None) -> Range.get extra (Esubst.reloc_rel n lft - 1)
+ | Inr (_, Some p) -> relevance_of_rel env p
+ end
| Var x -> relevance_of_var env x
| Sort _ | Ind _ | Prod _ -> Sorts.Relevant (* types are always relevant *)
| Cast (c, _, _) -> relevance_of_term_extra env extra lft subs c
| Lambda ({binder_relevance=r;_}, _, bdy) ->
- relevance_of_term_extra env (r::extra) (Esubst.el_lift lft) (Esubst.subs_lift subs) bdy
+ relevance_of_term_extra env (Range.cons r extra) (Esubst.el_lift lft) (Esubst.subs_lift subs) bdy
| LetIn ({binder_relevance=r;_}, _, _, bdy) ->
- relevance_of_term_extra env (r::extra) (Esubst.el_lift lft) (Esubst.subs_lift subs) bdy
+ relevance_of_term_extra env (Range.cons r extra) (Esubst.el_lift lft) (Esubst.subs_lift subs) bdy
| App (c, _) -> relevance_of_term_extra env extra lft subs c
| Const (c,_) -> relevance_of_constant env c
| Construct (c,_) -> relevance_of_constructor env c
@@ -115,5 +111,5 @@ let relevance_of_fterm env extra lft c =
let relevance_of_term env c =
if Environ.sprop_allowed env
- then relevance_of_term_extra env [] Esubst.el_id (Esubst.subs_id 0) c
+ then relevance_of_term_extra env Range.empty Esubst.el_id (Esubst.subs_id 0) c
else Sorts.Relevant
diff --git a/kernel/retypeops.mli b/kernel/retypeops.mli
index f4497be44b..dd4513959f 100644
--- a/kernel/retypeops.mli
+++ b/kernel/retypeops.mli
@@ -14,14 +14,14 @@
val relevance_of_term : Environ.env -> Constr.constr -> Sorts.relevance
-val relevance_of_fterm : Environ.env -> Sorts.relevance list ->
+val relevance_of_fterm : Environ.env -> Sorts.relevance Range.t ->
Esubst.lift -> CClosure.fconstr ->
Sorts.relevance
(** Helpers *)
open Names
-val relevance_of_rel_extra : Environ.env -> Sorts.relevance list -> int -> Sorts.relevance
+val relevance_of_rel : Environ.env -> int -> Sorts.relevance
val relevance_of_var : Environ.env -> Id.t -> Sorts.relevance
val relevance_of_constant : Environ.env -> Constant.t -> Sorts.relevance
val relevance_of_constructor : Environ.env -> constructor -> Sorts.relevance
diff --git a/plugins/ssr/ssrbool.v b/plugins/ssr/ssrbool.v
index 376410658a..f6b192c226 100644
--- a/plugins/ssr/ssrbool.v
+++ b/plugins/ssr/ssrbool.v
@@ -290,7 +290,7 @@ Require Import ssreflect ssrfun.
r -- a right-hand operation, as orb_andr : rightt_distributive orb andb.
T or t -- boolean truth, as in andbT: right_id true andb.
U -- predicate union, as in predU.
- W -- weakening, as in in1W : {in D, forall x, P} -> forall x, P. **)
+ W -- weakening, as in in1W : (forall x, P) -> {in D, forall x, P}. **)
Set Implicit Arguments.
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index f089b242a2..d2af957b54 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -264,16 +264,19 @@ let relevance_of_term env sigma c =
if Environ.sprop_allowed env then
let rec aux rels c =
match kind sigma c with
- | Rel n -> Retypeops.relevance_of_rel_extra env rels n
+ | Rel n ->
+ let len = Range.length rels in
+ if n <= len then Range.get rels (n - 1)
+ else Retypeops.relevance_of_rel env (n - len)
| Var x -> Retypeops.relevance_of_var env x
| Sort _ -> Sorts.Relevant
| Cast (c, _, _) -> aux rels c
| Prod ({binder_relevance=r}, _, codom) ->
- aux (r::rels) codom
+ aux (Range.cons r rels) codom
| Lambda ({binder_relevance=r}, _, bdy) ->
- aux (r::rels) bdy
+ aux (Range.cons r rels) bdy
| LetIn ({binder_relevance=r}, _, _, bdy) ->
- aux (r::rels) bdy
+ aux (Range.cons r rels) bdy
| App (c, _) -> aux rels c
| Const (c,_) -> Retypeops.relevance_of_constant env c
| Ind _ -> Sorts.Relevant
@@ -287,7 +290,7 @@ let relevance_of_term env sigma c =
| Meta _ | Evar _ -> Sorts.Relevant
in
- aux [] c
+ aux Range.empty c
else Sorts.Relevant
let relevance_of_type env sigma t =
diff --git a/test-suite/output/Arguments.out b/test-suite/output/Arguments.out
index 6704337f80..f889da4e98 100644
--- a/test-suite/output/Arguments.out
+++ b/test-suite/output/Arguments.out
@@ -1,7 +1,7 @@
Nat.sub : nat -> nat -> nat
Nat.sub is not universe polymorphic
-Arguments Nat.sub _%nat_scope _%nat_scope : simpl nomatch
+Arguments Nat.sub (_ _)%nat_scope : simpl nomatch
The reduction tactics unfold Nat.sub but avoid exposing match constructs
Nat.sub is transparent
Expands to: Constant Coq.Init.Nat.sub
@@ -25,7 +25,7 @@ Expands to: Constant Coq.Init.Nat.sub
Nat.sub : nat -> nat -> nat
Nat.sub is not universe polymorphic
-Arguments Nat.sub !_%nat_scope !_%nat_scope /
+Arguments Nat.sub (!_ !_)%nat_scope /
The reduction tactics unfold Nat.sub when the 1st and
2nd arguments evaluate to a constructor and when applied to 2 arguments
Nat.sub is transparent
@@ -33,7 +33,7 @@ Expands to: Constant Coq.Init.Nat.sub
Nat.sub : nat -> nat -> nat
Nat.sub is not universe polymorphic
-Arguments Nat.sub !_%nat_scope !_%nat_scope
+Arguments Nat.sub (!_ !_)%nat_scope
The reduction tactics unfold Nat.sub when the 1st and
2nd arguments evaluate to a constructor
Nat.sub is transparent
@@ -43,14 +43,14 @@ forall D1 C1 : Type,
(D1 -> C1) -> forall D2 C2 : Type, (D2 -> C2) -> D1 * D2 -> C1 * C2
pf is not universe polymorphic
-Arguments pf {D1%foo_scope} {C1%type_scope} _ [D2] [C2] : simpl never
+Arguments pf {D1}%foo_scope {C1}%type_scope _ [D2 C2] : simpl never
The reduction tactics never unfold pf
pf is transparent
Expands to: Constant Arguments.pf
fcomp : forall A B C : Type, (B -> C) -> (A -> B) -> A -> C
fcomp is not universe polymorphic
-Arguments fcomp {A%type_scope} {B%type_scope} {C%type_scope} _ _ _ /
+Arguments fcomp {A B C}%type_scope _ _ _ /
The reduction tactics unfold fcomp when applied to 6 arguments
fcomp is transparent
Expands to: Constant Arguments.fcomp
@@ -78,7 +78,7 @@ Expands to: Constant Arguments.S1.S2.f
f : forall T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat
f is not universe polymorphic
-Arguments f [T2%type_scope] _ _ !_%nat_scope !_ !_%nat_scope
+Arguments f [T2]%type_scope _ _ !_%nat_scope !_ !_%nat_scope
The reduction tactics unfold f when the 4th, 5th and
6th arguments evaluate to a constructor
f is transparent
@@ -86,7 +86,7 @@ Expands to: Constant Arguments.S1.f
f : forall T1 T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat
f is not universe polymorphic
-Arguments f [T1%type_scope] [T2%type_scope] _ _ !_%nat_scope !_ !_%nat_scope
+Arguments f [T1 T2]%type_scope _ _ !_%nat_scope !_ !_%nat_scope
The reduction tactics unfold f when the 5th, 6th and
7th arguments evaluate to a constructor
f is transparent
diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out
index 53d5624f6f..5093e785de 100644
--- a/test-suite/output/Arguments_renaming.out
+++ b/test-suite/output/Arguments_renaming.out
@@ -13,21 +13,21 @@ where
?y : [ |- nat]
Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x
-Arguments eq {A%type_scope}
-Arguments eq_refl {B%type_scope} {y}, [B] _
+Arguments eq {A}%type_scope
+Arguments eq_refl {B}%type_scope {y}, [B] _
eq_refl : forall (A : Type) (x : A), x = x
eq_refl is not universe polymorphic
-Arguments eq_refl {B%type_scope} {y}, [B] _
+Arguments eq_refl {B}%type_scope {y}, [B] _
Expands to: Constructor Coq.Init.Logic.eq_refl
Inductive myEq (B : Type) (x : A) : A -> Prop := myrefl : B -> myEq B x x
Arguments myEq _%type_scope
-Arguments myrefl {C%type_scope} x : rename
+Arguments myrefl {C}%type_scope x : rename
myrefl : forall (B : Type) (x : A), B -> myEq B x x
myrefl is not universe polymorphic
-Arguments myrefl {C%type_scope} x : rename
+Arguments myrefl {C}%type_scope x : rename
Expands to: Constructor Arguments_renaming.Test1.myrefl
myplus =
fix myplus (T : Type) (t : T) (n m : nat) {struct n} : nat :=
@@ -37,11 +37,11 @@ fix myplus (T : Type) (t : T) (n m : nat) {struct n} : nat :=
end
: forall T : Type, T -> nat -> nat -> nat
-Arguments myplus {Z%type_scope} !t !n%nat_scope m%nat_scope : rename
+Arguments myplus {Z}%type_scope !t (!n m)%nat_scope : rename
myplus : forall T : Type, T -> nat -> nat -> nat
myplus is not universe polymorphic
-Arguments myplus {Z%type_scope} !t !n%nat_scope m%nat_scope : rename
+Arguments myplus {Z}%type_scope !t (!n m)%nat_scope : rename
The reduction tactics unfold myplus when the 2nd and
3rd arguments evaluate to a constructor
myplus is transparent
@@ -51,12 +51,12 @@ Expands to: Constant Arguments_renaming.Test1.myplus
Inductive myEq (A B : Type) (x : A) : A -> Prop :=
myrefl : B -> myEq A B x x
-Arguments myEq _%type_scope _%type_scope
-Arguments myrefl A%type_scope {C%type_scope} x : rename
+Arguments myEq (_ _)%type_scope
+Arguments myrefl A%type_scope {C}%type_scope x : rename
myrefl : forall (A B : Type) (x : A), B -> myEq A B x x
myrefl is not universe polymorphic
-Arguments myrefl A%type_scope {C%type_scope} x : rename
+Arguments myrefl A%type_scope {C}%type_scope x : rename
Expands to: Constructor Arguments_renaming.myrefl
myrefl
: forall (A C : Type) (x : A), C -> myEq A C x x
@@ -68,11 +68,11 @@ fix myplus (T : Type) (t : T) (n m : nat) {struct n} : nat :=
end
: forall T : Type, T -> nat -> nat -> nat
-Arguments myplus {Z%type_scope} !t !n%nat_scope m%nat_scope : rename
+Arguments myplus {Z}%type_scope !t (!n m)%nat_scope : rename
myplus : forall T : Type, T -> nat -> nat -> nat
myplus is not universe polymorphic
-Arguments myplus {Z%type_scope} !t !n%nat_scope m%nat_scope : rename
+Arguments myplus {Z}%type_scope !t (!n m)%nat_scope : rename
The reduction tactics unfold myplus when the 2nd and
3rd arguments evaluate to a constructor
myplus is transparent
diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out
index 7489b8987e..e84ac85aa8 100644
--- a/test-suite/output/Cases.out
+++ b/test-suite/output/Cases.out
@@ -7,7 +7,7 @@ fix F (t : t) : P t :=
: forall P : t -> Type,
(let x := t in forall x0 : x, P x0 -> P (k x0)) -> forall t : t, P t
-Arguments t_rect _%function_scope _%function_scope
+Arguments t_rect (_ _)%function_scope
= fun d : TT => match d with
| {| f3 := b |} => b
end
@@ -26,7 +26,7 @@ match Nat.eq_dec x y with
end
: forall (x y : nat) (P : nat -> Type), P x -> P y -> P y
-Arguments proj _%nat_scope _%nat_scope _%function_scope
+Arguments proj (_ _)%nat_scope _%function_scope
foo =
fix foo (A : Type) (l : list A) {struct l} : option A :=
match l with
diff --git a/test-suite/output/Implicit.out b/test-suite/output/Implicit.out
index d65d2a8f55..5f22eb5d7c 100644
--- a/test-suite/output/Implicit.out
+++ b/test-suite/output/Implicit.out
@@ -5,7 +5,7 @@ ex_intro (P:=fun _ : nat => True) (x:=0) I
d2 = fun x : nat => d1 (y:=x)
: forall x x0 : nat, x0 = x -> x0 = x
-Arguments d2 [x%nat_scope] [x0%nat_scope]
+Arguments d2 [x x0]%nat_scope
map id (1 :: nil)
: list nat
map id' (1 :: nil)
diff --git a/test-suite/output/InitSyntax.out b/test-suite/output/InitSyntax.out
index ce058a6d34..da255e86cd 100644
--- a/test-suite/output/InitSyntax.out
+++ b/test-suite/output/InitSyntax.out
@@ -1,8 +1,8 @@
Inductive sig2 (A : Type) (P Q : A -> Prop) : Type :=
exist2 : forall x : A, P x -> Q x -> {x : A | P x & Q x}
-Arguments sig2 [A%type_scope] _%type_scope _%type_scope
-Arguments exist2 [A%type_scope] _%function_scope _%function_scope
+Arguments sig2 [A]%type_scope (_ _)%type_scope
+Arguments exist2 [A]%type_scope (_ _)%function_scope
exists x : nat, x = x
: Prop
fun b : bool => if b then b else b
diff --git a/test-suite/output/PatternsInBinders.out b/test-suite/output/PatternsInBinders.out
index 2952b6d94b..4f09f00c56 100644
--- a/test-suite/output/PatternsInBinders.out
+++ b/test-suite/output/PatternsInBinders.out
@@ -15,7 +15,7 @@ swap =
fun (A B : Type) '(x, y) => (y, x)
: forall A B : Type, A * B -> B * A
-Arguments swap {A%type_scope} {B%type_scope}
+Arguments swap {A B}%type_scope
fun (A B : Type) '(x, y) => swap (x, y) = (y, x)
: forall A B : Type, A * B -> Prop
forall (A B : Type) '(x, y), swap (x, y) = (y, x)
diff --git a/test-suite/output/PrintInfos.out b/test-suite/output/PrintInfos.out
index 7d0d81a3e8..71d162c314 100644
--- a/test-suite/output/PrintInfos.out
+++ b/test-suite/output/PrintInfos.out
@@ -1,24 +1,24 @@
existT : forall (A : Type) (P : A -> Type) (x : A), P x -> {x : A & P x}
existT is template universe polymorphic on sigT.u0 sigT.u1
-Arguments existT [A%type_scope] _%function_scope
+Arguments existT [A]%type_scope _%function_scope
Expands to: Constructor Coq.Init.Specif.existT
Inductive sigT (A : Type) (P : A -> Type) : Type :=
existT : forall x : A, P x -> {x : A & P x}
-Arguments sigT [A%type_scope] _%type_scope
-Arguments existT [A%type_scope] _%function_scope
+Arguments sigT [A]%type_scope _%type_scope
+Arguments existT [A]%type_scope _%function_scope
existT : forall (A : Type) (P : A -> Type) (x : A), P x -> {x : A & P x}
Argument A is implicit
Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x
-Arguments eq {A%type_scope}
-Arguments eq_refl {A%type_scope} {x}, [A] _
+Arguments eq {A}%type_scope
+Arguments eq_refl {A}%type_scope {x}, [A] _
eq_refl : forall (A : Type) (x : A), x = x
eq_refl is not universe polymorphic
-Arguments eq_refl {A%type_scope} {x}, [A] _
+Arguments eq_refl {A}%type_scope {x}, [A] _
Expands to: Constructor Coq.Init.Logic.eq_refl
eq_refl : forall (A : Type) (x : A), x = x
@@ -34,11 +34,11 @@ fix add (n m : nat) {struct n} : nat :=
end
: nat -> nat -> nat
-Arguments Nat.add _%nat_scope _%nat_scope
+Arguments Nat.add (_ _)%nat_scope
Nat.add : nat -> nat -> nat
Nat.add is not universe polymorphic
-Arguments Nat.add _%nat_scope _%nat_scope
+Arguments Nat.add (_ _)%nat_scope
Nat.add is transparent
Expands to: Constant Coq.Init.Nat.add
Nat.add : nat -> nat -> nat
@@ -52,9 +52,9 @@ Expands to: Constant Coq.Init.Peano.plus_n_O
Inductive le (n : nat) : nat -> Prop :=
le_n : n <= n | le_S : forall m : nat, n <= m -> n <= S m
-Arguments le _%nat_scope _%nat_scope
+Arguments le (_ _)%nat_scope
Arguments le_n _%nat_scope
-Arguments le_S {n%nat_scope} [m%nat_scope]
+Arguments le_S {n}%nat_scope [m]%nat_scope
comparison : Set
comparison is not universe polymorphic
@@ -80,8 +80,8 @@ Notation sym_eq := eq_sym
Expands to: Notation Coq.Init.Logic.sym_eq
Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x
-Arguments eq {A%type_scope}
-Arguments eq_refl {A%type_scope} {x}, {A} _
+Arguments eq {A}%type_scope
+Arguments eq_refl {A}%type_scope {x}, {A} _
n:nat
Hypothesis of the goal context.
diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out
index 298a0789c4..525ca48bee 100644
--- a/test-suite/output/UnivBinders.out
+++ b/test-suite/output/UnivBinders.out
@@ -33,7 +33,7 @@ fun (A : Type@{u}) (Wrap : Wrap@{u} A) => Wrap
: forall A : Type@{u}, Wrap@{u} A -> A
(* u |= *)
-Arguments wrap {A%type_scope} {Wrap}
+Arguments wrap {A}%type_scope {Wrap}
bar@{u} = nat
: Wrap@{u} Set
(* u |= Set < u *)
diff --git a/vernac/comArguments.ml b/vernac/comArguments.ml
index 737e0427ec..15077298aa 100644
--- a/vernac/comArguments.ml
+++ b/vernac/comArguments.ml
@@ -60,7 +60,7 @@ let warn_arguments_assert =
(* [nargs_for_red] is the number of arguments required to trigger reduction,
[args] is the main list of arguments statuses,
[more_implicits] is a list of extra lists of implicit statuses *)
-let vernac_arguments ~section_local reference args more_implicits nargs_for_red nargs_before_bidi flags =
+let vernac_arguments ~section_local reference args more_implicits flags =
let env = Global.env () in
let sigma = Evd.from_env env in
let assert_flag = List.mem `Assert flags in
@@ -83,6 +83,23 @@ let vernac_arguments ~section_local reference args more_implicits nargs_for_red
if clear_implicits_flag && default_implicits_flag then
err_incompat "clear implicits" "default implicits";
+ let args, nargs_for_red, nargs_before_bidi, _i =
+ List.fold_left (fun (args,red,bidi,i) arg ->
+ match arg with
+ | RealArg arg -> (arg::args,red,bidi,i+1)
+ | VolatileArg ->
+ if Option.has_some red
+ then CErrors.user_err Pp.(str "The \"/\" modifier may only occur once.");
+ (args,Some i,bidi,i)
+ | BidiArg ->
+ if Option.has_some bidi
+ then CErrors.user_err Pp.(str "The \"&\" modifier may only occur once.");
+ (args,red,Some i,i))
+ ([],None,None,0)
+ args
+ in
+ let args = List.rev args in
+
let sr = smart_global reference in
let inf_names =
let ty, _ = Typeops.type_of_global_in_context env sr in
diff --git a/vernac/comArguments.mli b/vernac/comArguments.mli
index f78e01a11f..71effddf67 100644
--- a/vernac/comArguments.mli
+++ b/vernac/comArguments.mli
@@ -13,7 +13,5 @@ val vernac_arguments
-> Libnames.qualid Constrexpr.or_by_notation
-> Vernacexpr.vernac_argument_status list
-> (Names.Name.t * Impargs.implicit_kind) list list
- -> int option
- -> int option
-> Vernacexpr.arguments_modifier list
-> unit
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 0515e88a15..5b97e06b2b 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -781,25 +781,8 @@ GRAMMAR EXTEND Gram
];
mods = OPT [ ":"; l = LIST1 arguments_modifier SEP "," -> { l } ] ->
{ let mods = match mods with None -> [] | Some l -> List.flatten l in
- let slash_position = ref None in
- let ampersand_position = ref None in
- let rec parse_args i = function
- | [] -> []
- | `Id x :: args -> x :: parse_args (i+1) args
- | `Slash :: args ->
- if Option.is_empty !slash_position then
- (slash_position := Some i; parse_args i args)
- else
- user_err Pp.(str "The \"/\" modifier can occur only once")
- | `Ampersand :: args ->
- if Option.is_empty !ampersand_position then
- (ampersand_position := Some i; parse_args i args)
- else
- user_err Pp.(str "The \"&\" modifier can occur only once")
- in
- let args = parse_args 0 (List.flatten args) in
let more_implicits = Option.default [] more_implicits in
- VernacArguments (qid, args, more_implicits, !slash_position, !ampersand_position, mods) }
+ VernacArguments (qid, List.flatten args, more_implicits, mods) }
| IDENT "Implicit"; "Type"; bl = reserv_list ->
{ VernacReserve bl }
@@ -843,17 +826,17 @@ GRAMMAR EXTEND Gram
argument_spec_block: [
[ item = argument_spec ->
{ let name, recarg_like, notation_scope = item in
- [`Id { name=name; recarg_like=recarg_like;
+ [RealArg { name=name; recarg_like=recarg_like;
notation_scope=notation_scope;
implicit_status = NotImplicit}] }
- | "/" -> { [`Slash] }
- | "&" -> { [`Ampersand] }
+ | "/" -> { [VolatileArg] }
+ | "&" -> { [BidiArg] }
| "("; items = LIST1 argument_spec; ")"; sc = OPT scope_delimiter ->
{ let f x = match sc, x with
| None, x -> x | x, None -> Option.map (fun y -> CAst.make ~loc y) x
| Some _, Some _ -> user_err Pp.(str "scope declared twice") in
List.map (fun (name,recarg_like,notation_scope) ->
- `Id { name=name; recarg_like=recarg_like;
+ RealArg { name=name; recarg_like=recarg_like;
notation_scope=f notation_scope;
implicit_status = NotImplicit}) items }
| "["; items = LIST1 argument_spec; "]"; sc = OPT scope_delimiter ->
@@ -861,7 +844,7 @@ GRAMMAR EXTEND Gram
| None, x -> x | x, None -> Option.map (fun y -> CAst.make ~loc y) x
| Some _, Some _ -> user_err Pp.(str "scope declared twice") in
List.map (fun (name,recarg_like,notation_scope) ->
- `Id { name=name; recarg_like=recarg_like;
+ RealArg { name=name; recarg_like=recarg_like;
notation_scope=f notation_scope;
implicit_status = Implicit}) items }
| "{"; items = LIST1 argument_spec; "}"; sc = OPT scope_delimiter ->
@@ -869,7 +852,7 @@ GRAMMAR EXTEND Gram
| None, x -> x | x, None -> Option.map (fun y -> CAst.make ~loc y) x
| Some _, Some _ -> user_err Pp.(str "scope declared twice") in
List.map (fun (name,recarg_like,notation_scope) ->
- `Id { name=name; recarg_like=recarg_like;
+ RealArg { name=name; recarg_like=recarg_like;
notation_scope=f notation_scope;
implicit_status = MaximallyImplicit}) items }
]
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index 3dbf7afb78..080629ede2 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -1068,39 +1068,52 @@ let string_of_definition_object_kind = let open Decls in function
| Some Flags.Current -> [SetOnlyParsing]
| Some v -> [SetCompatVersion v]))
)
- | VernacArguments (q, args, more_implicits, nargs, nargs_before_bidi, mods) ->
+ | VernacArguments (q, args, more_implicits, mods) ->
return (
hov 2 (
keyword "Arguments" ++ spc() ++
pr_smart_global q ++
let pr_s = function None -> str"" | Some {v=s} -> str "%" ++ str s in
let pr_if b x = if b then x else str "" in
- let pr_br imp x = match imp with
- | Impargs.Implicit -> str "[" ++ x ++ str "]"
- | Impargs.MaximallyImplicit -> str "{" ++ x ++ str "}"
- | Impargs.NotImplicit -> x in
- let rec print_arguments n nbidi l =
- match n, nbidi, l with
- | Some 0, _, l -> spc () ++ str"/" ++ print_arguments None nbidi l
- | _, Some 0, l -> spc () ++ str"&" ++ print_arguments n None l
- | None, None, [] -> mt()
- | _, _, [] ->
- let dummy = {name=Anonymous; recarg_like=false;
- notation_scope=None; implicit_status=Impargs.NotImplicit}
- in
- print_arguments n nbidi [dummy]
- | n, nbidi, { name = id; recarg_like = k;
+ let pr_one_arg (x,k) = pr_if k (str"!") ++ Name.print x in
+ let pr_br imp force x =
+ let left,right =
+ match imp with
+ | Impargs.Implicit -> str "[", str "]"
+ | Impargs.MaximallyImplicit -> str "{", str "}"
+ | Impargs.NotImplicit -> if force then str"(",str")" else mt(),mt()
+ in
+ left ++ x ++ right
+ in
+ let get_arguments_like s imp tl =
+ if s = None && imp = Impargs.NotImplicit then [], tl
+ else
+ let rec fold extra = function
+ | RealArg arg :: tl when
+ Option.equal (fun a b -> String.equal a.CAst.v b.CAst.v) arg.notation_scope s
+ && arg.implicit_status = imp ->
+ fold ((arg.name,arg.recarg_like) :: extra) tl
+ | args -> List.rev extra, args
+ in
+ fold [] tl
+ in
+ let rec print_arguments = function
+ | [] -> mt()
+ | VolatileArg :: l -> spc () ++ str"/" ++ print_arguments l
+ | BidiArg :: l -> spc () ++ str"&" ++ print_arguments l
+ | RealArg { name = id; recarg_like = k;
notation_scope = s;
implicit_status = imp } :: tl ->
- spc() ++ pr_br imp (pr_if k (str"!") ++ Name.print id ++ pr_s s) ++
- print_arguments (Option.map pred n) (Option.map pred nbidi) tl
+ let extra, tl = get_arguments_like s imp tl in
+ spc() ++ pr_br imp (extra<>[]) (prlist_with_sep spc pr_one_arg ((id,k)::extra)) ++
+ pr_s s ++ print_arguments tl
in
let rec print_implicits = function
| [] -> mt ()
| (name, impl) :: rest ->
- spc() ++ pr_br impl (Name.print name) ++ print_implicits rest
+ spc() ++ pr_br impl false (Name.print name) ++ print_implicits rest
in
- print_arguments nargs nargs_before_bidi args ++
+ print_arguments args ++
if not (List.is_empty more_implicits) then
prlist (fun l -> str"," ++ print_implicits l) more_implicits
else (mt ()) ++
diff --git a/vernac/prettyp.ml b/vernac/prettyp.ml
index 5ebc89892c..ea49cae9db 100644
--- a/vernac/prettyp.ml
+++ b/vernac/prettyp.ml
@@ -259,6 +259,13 @@ let implicit_kind_of_status = function
| None -> Anonymous, NotImplicit
| Some (id,_,(maximal,_)) -> Name id, if maximal then MaximallyImplicit else Implicit
+let dummy = {
+ Vernacexpr.implicit_status = NotImplicit;
+ name = Anonymous;
+ recarg_like = false;
+ notation_scope = None;
+}
+
let is_dummy {Vernacexpr.implicit_status; name; recarg_like; notation_scope} =
name = Anonymous && not recarg_like && notation_scope = None && implicit_status = NotImplicit
@@ -287,6 +294,20 @@ let rec main_implicits i renames recargs scopes impls =
then [] (* we may have a trail of dummies due to eg "clear scopes" *)
else status :: rest
+let rec insert_fake_args volatile bidi impls =
+ let open Vernacexpr in
+ match volatile, bidi with
+ | Some 0, _ -> VolatileArg :: insert_fake_args None bidi impls
+ | _, Some 0 -> BidiArg :: insert_fake_args volatile None impls
+ | None, None -> List.map (fun a -> RealArg a) impls
+ | _, _ ->
+ let hd, tl = match impls with
+ | impl :: impls -> impl, impls
+ | [] -> dummy, []
+ in
+ let f = Option.map pred in
+ RealArg hd :: insert_fake_args (f volatile) (f bidi) tl
+
let print_arguments ref =
let qid = Nametab.shortest_qualid_of_global Id.Set.empty ref in
let flags, recargs, nargs_for_red =
@@ -312,12 +333,13 @@ let print_arguments ref =
let impls = main_implicits 0 renames recargs scopes impls in
let moreimpls = List.map (fun (_,i) -> List.map implicit_kind_of_status i) moreimpls in
let bidi = Pretyping.get_bidirectionality_hint ref in
- if impls = [] && moreimpls = [] && nargs_for_red = None && bidi = None && flags = [] then []
+ let impls = insert_fake_args nargs_for_red bidi impls in
+ if impls = [] && moreimpls = [] && flags = [] then []
else
let open Constrexpr in
let open Vernacexpr in
[Ppvernac.pr_vernac_expr
- (VernacArguments (CAst.make (AN qid), impls, moreimpls, nargs_for_red, bidi, flags))]
+ (VernacArguments (CAst.make (AN qid), impls, moreimpls, flags))]
let print_name_infos ref =
let type_info_for_implicit =
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index f56cc00c3b..535aceed15 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -2167,10 +2167,10 @@ let translate_vernac ~atts v = let open Vernacextend in match v with
vernac_hints ~atts dbnames hints)
| VernacSyntacticDefinition (id,c,b) ->
VtDefault(fun () -> vernac_syntactic_definition ~atts id c b)
- | VernacArguments (qid, args, more_implicits, nargs, bidi, flags) ->
+ | VernacArguments (qid, args, more_implicits, flags) ->
VtDefault(fun () ->
with_section_locality ~atts
- (ComArguments.vernac_arguments qid args more_implicits nargs bidi flags))
+ (ComArguments.vernac_arguments qid args more_implicits flags))
| VernacReserve bl ->
VtDefault(fun () ->
unsupported_attributes atts;
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index 564c55670d..ce96d9265c 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -250,13 +250,17 @@ type vernac_cumulative = VernacCumulative | VernacNonCumulative
(** {6 The type of vernacular expressions} *)
-type vernac_argument_status = {
+type vernac_one_argument_status = {
name : Name.t;
recarg_like : bool;
notation_scope : string CAst.t option;
implicit_status : Impargs.implicit_kind;
}
+type vernac_argument_status =
+ | VolatileArg | BidiArg
+ | RealArg of vernac_one_argument_status
+
type arguments_modifier =
[ `Assert
| `ClearBidiHint
@@ -383,8 +387,6 @@ type nonrec vernac_expr =
qualid or_by_notation *
vernac_argument_status list (* Main arguments status list *) *
(Name.t * Impargs.implicit_kind) list list (* Extra implicit status lists *) *
- int option (* Number of args to trigger reduction *) *
- int option (* Number of args before bidirectional typing *) *
arguments_modifier list
| VernacReserve of simple_binder list
| VernacGeneralizable of (lident list) option
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 08:04:11 +0000