aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--config/dune2
-rw-r--r--configure.ml2
-rw-r--r--dev/ci/docker/README.md31
-rw-r--r--doc/sphinx/addendum/extraction.rst2
-rw-r--r--doc/sphinx/addendum/generalized-rewriting.rst2
-rw-r--r--doc/sphinx/biblio.bib2
-rw-r--r--doc/sphinx/language/cic.rst11
-rw-r--r--doc/sphinx/language/gallina-specification-language.rst15
-rw-r--r--doc/sphinx/proof-engine/ssreflect-proof-language.rst7
-rw-r--r--ide/coqide.ml2
-rw-r--r--ide/session.ml6
-rw-r--r--ide/session.mli2
-rw-r--r--kernel/byterun/dune14
-rw-r--r--parsing/g_constr.mlg11
-rw-r--r--plugins/ltac/g_tactic.mlg8
-rw-r--r--printing/ppconstr.ml3
-rw-r--r--test-suite/bugs/closed/bug_10060.v15
-rw-r--r--test-suite/output/Notations4.out2
-rw-r--r--test-suite/output/Notations4.v7
-rw-r--r--user-contrib/Ltac2/g_ltac2.mlg4
-rw-r--r--vernac/declaremods.ml2
-rw-r--r--vernac/g_vernac.mlg18
22 files changed, 106 insertions, 62 deletions
diff --git a/config/dune b/config/dune
index c146e7df67..a303774e17 100644
--- a/config/dune
+++ b/config/dune
@@ -7,7 +7,7 @@
; Dune doesn't use configure's output, but it is still necessary for
; some Coq files to work; will be fixed in the future.
(rule
- (targets coq_config.ml coq_config.py Makefile)
+ (targets coq_config.ml coq_config.py Makefile dune.c_flags)
(mode fallback)
(deps %{project_root}/configure.ml %{project_root}/dev/ocamldebug-coq.run (env_var COQ_CONFIGURE_PREFIX))
(action (chdir %{project_root} (run %{ocaml} configure.ml -no-ask -native-compiler no))))
diff --git a/configure.ml b/configure.ml
index a53292b4cf..411578445c 100644
--- a/configure.ml
+++ b/configure.ml
@@ -1216,7 +1216,7 @@ let write_dune_c_flags f =
close_out o;
Unix.chmod f 0o444
-let _ = try write_dune_c_flags "kernel/byterun/dune.c_flags" with _ -> ()
+let _ = write_dune_c_flags "config/dune.c_flags"
let write_macos_metadata exec =
let f = "config/Info-"^exec^".plist" in
diff --git a/dev/ci/docker/README.md b/dev/ci/docker/README.md
index 919e2a735f..16c4ac37d9 100644
--- a/dev/ci/docker/README.md
+++ b/dev/ci/docker/README.md
@@ -4,10 +4,33 @@ This directory provides Docker images to be used by Coq's CI. The
images do support Docker autobuild on `hub.docker.com` and Gitlab's
private registry.
-Gitlab CI will build and tag a Docker by default for every job if the
-`SKIP_DOCKER` variable is not set to `false`. In Coq's CI, this
-variable is usually set to `false` indeed to avoid booting a useless
-job.
+The Gitlab CI will build a docker image unless the CI environment variable
+`SKIP_DOCKER` is set to `true`. This image will be
+stored in the [Gitlab container registry](https://gitlab.com/coq/coq/container_registry)
+under the name given by the `CACHEKEY` variable from
+the [Gitlab CI configuration file](../../../.gitlab-ci.yml).
+
+In Coq's default CI, `SKIP_DOCKER` is set so as to avoid running a lengthy redundant job.
+
+It can be used to regenerate a fresh Docker image on Gitlab through the following steps.
+- Change the `CACHEKEY` variable to a fresh name in the CI configuration in a new commit.
+- Push this commit to a Github PR. This will trigger a Gitlab CI run that will
+ immediately fail, as the Docker image is missing and the `SKIP_DOCKER`
+ default value prevents rebuilding the image.
+- Run a new pipeline on Gitlab with that PR branch, using the green "Run pipeline"
+ button on the [web interface](https://gitlab.com/coq/coq/pipelines),
+ with the `SKIP_DOCKER` environment variable set to `false`. This will run a `docker-boot` process, and
+ once completed, a new Docker image will be available in the container registry,
+ with the name set in `CACHEKEY`.
+- Any pipeline with the same `CACHEKEY` will now automatically reuse that
+ image without rebuilding it from scratch.
+
+For documentation purposes, we also require keeping in sync the `CACHEKEY` comment
+from the first line of the [Dockerfile](bionic_coq/Dockerfile) in the same
+commit.
+
+In case you do not have the rights to run Gitlab CI pipelines, you should ask
+the ci-maintainers Github team to do it for you.
## Manual Building
diff --git a/doc/sphinx/addendum/extraction.rst b/doc/sphinx/addendum/extraction.rst
index 9f92fc4c56..0754145b39 100644
--- a/doc/sphinx/addendum/extraction.rst
+++ b/doc/sphinx/addendum/extraction.rst
@@ -530,7 +530,7 @@ A detailed example: Euclidean division
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The file ``Euclid`` contains the proof of Euclidean division.
-The natural numbers used here are unary, represented by the type``nat``,
+The natural numbers used here are unary, represented by the type ``nat``,
which is defined by two constructors ``O`` and ``S``.
This module contains a theorem ``eucl_dev``, whose type is::
diff --git a/doc/sphinx/addendum/generalized-rewriting.rst b/doc/sphinx/addendum/generalized-rewriting.rst
index 93a1be027c..4feda5e875 100644
--- a/doc/sphinx/addendum/generalized-rewriting.rst
+++ b/doc/sphinx/addendum/generalized-rewriting.rst
@@ -117,7 +117,7 @@ parameters is any term :math:`f \, t_1 \ldots t_n`.
.. example:: Morphisms
Continuing the previous example, let ``union: forall (A : Type), list A -> list A -> list A``
- perform the union of two sets by appending one list to the other. ``union` is a binary
+ perform the union of two sets by appending one list to the other. ``union`` is a binary
morphism parametric over ``A`` that respects the relation instance
``(set_eq A)``. The latter condition is proved by showing:
diff --git a/doc/sphinx/biblio.bib b/doc/sphinx/biblio.bib
index db089df395..3d73f9bd6e 100644
--- a/doc/sphinx/biblio.bib
+++ b/doc/sphinx/biblio.bib
@@ -192,7 +192,7 @@ s},
@InProceedings{Del00,
author = {Delahaye, D.},
- title = {A {T}actic {L}anguage for the {S}ystem {{\sf Coq}}},
+ title = {A {T}actic {L}anguage for the {S}ystem {Coq}},
booktitle = {Proceedings of Logic for Programming and Automated Reasoning
(LPAR), Reunion Island},
publisher = SV,
diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst
index 54aeed428f..4beaff70f5 100644
--- a/doc/sphinx/language/cic.rst
+++ b/doc/sphinx/language/cic.rst
@@ -1200,7 +1200,8 @@ Conversion is preserved as any (partial) instance :math:`I_j~q_1 … q_r` or
at level :math:`\Type` (without annotations or hiding it behind a
definition) template polymorphic if possible.
- This can be prevented using the ``notemplate`` attribute.
+ This can be prevented using the ``universes(notemplate)``
+ attribute.
.. warn:: Automatically declaring @ident as template polymorphic.
@@ -1208,9 +1209,9 @@ Conversion is preserved as any (partial) instance :math:`I_j~q_1 … q_r` or
implicitly declared template polymorphic by :flag:`Auto Template
Polymorphism`.
- An inductive type can be forced to be template polymorphic using the
- ``template`` attribute: it should then fulfill the criterion to
- be template polymorphic or an error is raised.
+ An inductive type can be forced to be template polymorphic using
+ the ``universes(template)`` attribute: it should then fulfill the
+ criterion to be template polymorphic or an error is raised.
.. exn:: Inductive @ident cannot be made template polymorphic.
@@ -1221,7 +1222,7 @@ Conversion is preserved as any (partial) instance :math:`I_j~q_1 … q_r` or
Template polymorphism and universe polymorphism (see Chapter
:ref:`polymorphicuniverses`) are incompatible, so if the later is
enabled it will prevail over automatic template polymorphism and
- cause an error when using the ``template`` attribute.
+ cause an error when using the ``universes(template)`` attribute.
.. flag:: Template Check
diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst
index f667dd94b0..94e9ccf0d4 100644
--- a/doc/sphinx/language/gallina-specification-language.rst
+++ b/doc/sphinx/language/gallina-specification-language.rst
@@ -1503,19 +1503,20 @@ Each attribute has a name (an identifier) and may have a value.
A value is either a :token:`string` (in which case it is specified with an equal ``=`` sign),
or a list of attributes, enclosed within brackets.
-Currently,
-the following attributes names are recognized:
+Some attributes are specific to a command, and so are described with
+that command. Currently, the following attributes are recognized by a
+variety of commands:
-``monomorphic``, ``polymorphic``
- Take no value, analogous to the ``Monomorphic`` and ``Polymorphic`` flags
- (see :ref:`polymorphicuniverses`).
+``universes(monomorphic)``, ``universes(polymorphic)``
+ Equivalent to the ``Monomorphic`` and
+ ``Polymorphic`` flags (see :ref:`polymorphicuniverses`).
``program``
- Takes no value, analogous to the ``Program`` flag
+ Takes no value, equivalent to the ``Program`` flag
(see :ref:`programs`).
``global``, ``local``
- Take no value, analogous to the ``Global`` and ``Local`` flags
+ Take no value, equivalent to the ``Global`` and ``Local`` flags
(see :ref:`controlling-locality-of-commands`).
``deprecated``
diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
index 4c697be963..853ddfd6dc 100644
--- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst
+++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
@@ -1513,7 +1513,7 @@ In a goal like the following::
=============
m < 5 + n
-The tactic ``abstract: abs n`` first generalizes the goal with respect ton
+The tactic :g:`abstract: abs n` first generalizes the goal with respect to :g:`n`
(that is not visible to the abstract constant abs) and then assigns
abs. The resulting goal is::
@@ -4071,6 +4071,7 @@ which the function is supplied:
:name: congr
This tactic:
+
+ checks that the goal is a Leibniz equality;
+ matches both sides of this equality with “term applied to some arguments”, inferring the right number of arguments from the goal and the type of term. This may expand some definitions or fixpoints;
+ generates the subgoals corresponding to pairwise equalities of the arguments present in the goal.
@@ -4218,7 +4219,7 @@ in the second column.
``ident`` in all the occurrences of ``term2``
* - ``term1 as ident in term2``
- ``term 1``
- - in all the subterms identified by ``ident`
+ - in all the subterms identified by ``ident``
in all the occurrences of ``term2[term 1 /ident]``
The rewrite tactic supports two more patterns obtained prefixing the
@@ -5023,7 +5024,7 @@ mechanism:
Coercion is_true (b : bool) := b = true.
This allows any boolean formula ``b`` to be used in a context where |Coq|
-would expect a proposition, e.g., after ``Lemma … : ``. It is then
+would expect a proposition, e.g., after ``Lemma … :``. It is then
interpreted as ``(is_true b)``, i.e., the proposition ``b = true``. Coercions
are elided by the pretty-printer, so they are essentially transparent
to the user.
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 70fa61b208..14cd87e7b5 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -966,6 +966,8 @@ let build_ui () =
with _ -> ()
in
let _ = w#event#connect#delete ~callback:(fun _ -> File.quit ~parent:w (); true) in
+ let _ = w#misc#connect#size_allocate
+ ~callback:(fun rect -> window_size := (rect.Gtk.width, rect.Gtk.height)) in
let _ = set_drag w#drag in
let vbox = GPack.vbox ~homogeneous:false ~packing:w#add () in
diff --git a/ide/session.ml b/ide/session.ml
index 38fdd0ef2a..2824530c43 100644
--- a/ide/session.ml
+++ b/ide/session.ml
@@ -432,6 +432,8 @@ let kill (sn:session) =
sn.script#destroy ();
Coq.close_coqtop sn.coqtop
+let window_size = ref (window_width#get, window_height#get)
+
let build_layout (sn:session) =
let session_paned = GPack.paned `VERTICAL () in
let session_box =
@@ -514,9 +516,9 @@ let build_layout (sn:session) =
iteration of the loop *)
let () =
(* 14 is the estimated size for vertical borders *)
- let estimated_vertical_handle_position = (window_width#get - 14) / 2 in
+ let estimated_vertical_handle_position = (fst !window_size - 14) / 2 in
(* 169 is the estimated size for menus, command line, horizontal border *)
- let estimated_horizontal_handle_position = (window_height#get - 169) / 2 in
+ let estimated_horizontal_handle_position = (snd !window_size - 169) / 2 in
if estimated_vertical_handle_position > 0 then
eval_paned#set_position estimated_vertical_handle_position;
if estimated_horizontal_handle_position > 0 then
diff --git a/ide/session.mli b/ide/session.mli
index f5d8d7c991..63ac1e6dc0 100644
--- a/ide/session.mli
+++ b/ide/session.mli
@@ -51,3 +51,5 @@ val kill : session -> unit
val build_layout : session ->
GObj.widget option * GObj.widget option * GObj.widget
+
+val window_size : (int * int) ref
diff --git a/kernel/byterun/dune b/kernel/byterun/dune
index d0145176ea..8d8374a603 100644
--- a/kernel/byterun/dune
+++ b/kernel/byterun/dune
@@ -1,20 +1,8 @@
-; Dune doesn't use configure's output, but it is still necessary for
-; some Coq files to work; will be fixed in the future.
-(rule
- (targets dune.c_flags)
- (mode fallback)
- (deps %{project_root}/configure.ml %{project_root}/dev/ocamldebug-coq.run (env_var COQ_CONFIGURE_PREFIX))
- (action (chdir %{project_root} (run %{ocaml} configure.ml -no-ask -native-compiler no))))
-
-(env
- (dev (c_flags (:include dune.c_flags)))
- (release (c_flags (:include dune.c_flags)))
- (ireport (c_flags (:include dune.c_flags))))
-
(library
(name byterun)
(synopsis "Coq's Kernel Abstract Reduction Machine [C implementation]")
(public_name coq.vm)
+ (c_flags (:include %{project_root}/config/dune.c_flags))
(c_names coq_fix_code coq_memory coq_values coq_interp))
(rule
diff --git a/parsing/g_constr.mlg b/parsing/g_constr.mlg
index 470782a7dc..b1d530438d 100644
--- a/parsing/g_constr.mlg
+++ b/parsing/g_constr.mlg
@@ -244,17 +244,17 @@ GRAMMAR EXTEND Gram
] ]
;
record_declaration:
- [ [ fs = record_fields -> { CAst.make ~loc @@ CRecord fs } ] ]
+ [ [ fs = record_fields_instance -> { CAst.make ~loc @@ CRecord fs } ] ]
;
- record_fields:
- [ [ f = record_field_declaration; ";"; fs = record_fields -> { f :: fs }
- | f = record_field_declaration -> { [f] }
+ record_fields_instance:
+ [ [ f = record_field_instance; ";"; fs = record_fields_instance -> { f :: fs }
+ | f = record_field_instance -> { [f] }
| -> { [] }
] ]
;
- record_field_declaration:
+ record_field_instance:
[ [ id = global; bl = binders; ":="; c = lconstr ->
{ (id, mkLambdaCN ~loc bl c) } ] ]
;
@@ -393,7 +393,6 @@ GRAMMAR EXTEND Gram
;
record_patterns:
[ [ p = record_pattern; ";"; ps = record_patterns -> { p :: ps }
- | p = record_pattern; ";" -> { [p] }
| p = record_pattern-> { [p] }
| -> { [] }
] ]
diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg
index 1b00a93834..eb282d1f83 100644
--- a/plugins/ltac/g_tactic.mlg
+++ b/plugins/ltac/g_tactic.mlg
@@ -439,7 +439,7 @@ GRAMMAR EXTEND Gram
[ [ "in"; id = id_or_meta; ipat = as_ipat -> { Some (id,ipat) }
| -> { None } ] ]
;
- orient:
+ orient_rw:
[ [ "->" -> { true }
| "<-" -> { false }
| -> { true } ] ]
@@ -451,10 +451,10 @@ GRAMMAR EXTEND Gram
] ]
;
fixdecl:
- [ [ "("; id = ident; bl=LIST0 simple_binder; ann=fixannot;
+ [ [ "("; id = ident; bl=LIST0 simple_binder; ann=struct_annot;
":"; ty=lconstr; ")" -> { (loc, id, bl, ann, ty) } ] ]
;
- fixannot:
+ struct_annot:
[ [ "{"; IDENT "struct"; id=name; "}" -> { Some id }
| -> { None } ] ]
;
@@ -506,7 +506,7 @@ GRAMMAR EXTEND Gram
] ]
;
oriented_rewriter :
- [ [ b = orient; p = rewriter -> { let (m,c) = p in (b,m,c) } ] ]
+ [ [ b = orient_rw; p = rewriter -> { let (m,c) = p in (b,m,c) } ] ]
;
induction_clause:
[ [ c = destruction_arg; pat = as_or_and_ipat; eq = eqn_ipat;
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 5ed96dd5e3..2da163b8ee 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -249,7 +249,8 @@ let tag_var = tag Tag.variable
let pp (c, p) =
pr_reference c ++ spc() ++ str ":=" ++ pr_patt spc (lpatrec, Any) p
in
- str "{| " ++ prlist_with_sep pr_semicolon pp l ++ str " |}", lpatrec
+ (if l = [] then str "{| |}"
+ else str "{| " ++ prlist_with_sep pr_semicolon pp l ++ str " |}"), lpatrec
| CPatAlias (p, na) ->
pr_patt mt (las,E) p ++ str " as " ++ pr_lname na, las
diff --git a/test-suite/bugs/closed/bug_10060.v b/test-suite/bugs/closed/bug_10060.v
new file mode 100644
index 0000000000..d74f6e388b
--- /dev/null
+++ b/test-suite/bugs/closed/bug_10060.v
@@ -0,0 +1,15 @@
+Module Type T.
+ Parameter b : Set.
+End T.
+
+Module M1(N : T).
+End M1.
+
+Module M2.
+End M2.
+
+Section S.
+ Variable a : Set.
+ Definition b := a.
+ Fail Include M1.
+End S.
diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out
index c1b9a2b1c6..ba4ac5a8f9 100644
--- a/test-suite/output/Notations4.out
+++ b/test-suite/output/Notations4.out
@@ -57,3 +57,5 @@ where
|- 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)
+fun '{| |} => true
+ : R -> bool
diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v
index d1063bfd04..4b9d0abd95 100644
--- a/test-suite/output/Notations4.v
+++ b/test-suite/output/Notations4.v
@@ -133,3 +133,10 @@ Check fun y : nat => # (x,z) |-> y & y.
Check fun y : nat => # (x,z) |-> (x + y) & (y + z).
End K.
+
+Module EmptyRecordSyntax.
+
+Record R := { n : nat }.
+Check fun '{|n:=x|} => true.
+
+End EmptyRecordSyntax.
diff --git a/user-contrib/Ltac2/g_ltac2.mlg b/user-contrib/Ltac2/g_ltac2.mlg
index cc3a7c0f79..c1bd585f3f 100644
--- a/user-contrib/Ltac2/g_ltac2.mlg
+++ b/user-contrib/Ltac2/g_ltac2.mlg
@@ -643,7 +643,7 @@ GRAMMAR EXTEND Gram
q_conversion:
[ [ c = conversion -> { c } ] ]
;
- orient:
+ ltac2_orient:
[ [ "->" -> { CAst.make ~loc (Some true) }
| "<-" -> { CAst.make ~loc (Some false) }
| -> { CAst.make ~loc None }
@@ -665,7 +665,7 @@ GRAMMAR EXTEND Gram
] ]
;
oriented_rewriter:
- [ [ b = orient; r = rewriter ->
+ [ [ b = ltac2_orient; r = rewriter ->
{ let (m, c) = r in
CAst.make ~loc @@ {
rew_orient = b;
diff --git a/vernac/declaremods.ml b/vernac/declaremods.ml
index 65cd4cd6a4..54dda09e83 100644
--- a/vernac/declaremods.ml
+++ b/vernac/declaremods.ml
@@ -972,6 +972,8 @@ let declare_modtype id args mtys mty_l =
protect_summaries declare_mt
let declare_include me_asts =
+ if Global.sections_are_opened () then
+ user_err Pp.(str "Include is not allowed inside sections.");
protect_summaries (fun _ -> RawIncludeOps.declare_include me_asts)
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 4243d0c911..a78f4645c2 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -51,6 +51,7 @@ let decl_notation = Entry.create "vernac:decl_notation"
let record_field = Entry.create "vernac:record_field"
let of_type_with_opt_coercion = Entry.create "vernac:of_type_with_opt_coercion"
let section_subset_expr = Entry.create "vernac:section_subset_expr"
+let scope_delimiter = Entry.create "vernac:scope_delimiter"
let make_bullet s =
let open Proof_bullet in
@@ -717,7 +718,7 @@ END
(* Extensions: implicits, coercions, etc. *)
GRAMMAR EXTEND Gram
- GLOBAL: gallina_ext hint_info;
+ GLOBAL: gallina_ext hint_info scope_delimiter;
gallina_ext:
[ [ (* Transparent and Opaque *)
@@ -835,11 +836,11 @@ GRAMMAR EXTEND Gram
{ [`ClearImplicits; `ClearScopes] }
] ]
;
- scope:
+ scope_delimiter:
[ [ "%"; key = IDENT -> { key } ] ]
;
argument_spec: [
- [ b = OPT "!"; id = name ; s = OPT scope ->
+ [ b = OPT "!"; id = name ; s = OPT scope_delimiter ->
{ id.CAst.v, not (Option.is_empty b), Option.map (fun x -> CAst.make ~loc x) s }
]
];
@@ -852,7 +853,7 @@ GRAMMAR EXTEND Gram
implicit_status = NotImplicit}] }
| "/" -> { [`Slash] }
| "&" -> { [`Ampersand] }
- | "("; items = LIST1 argument_spec; ")"; sc = OPT scope ->
+ | "("; 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
@@ -860,7 +861,7 @@ GRAMMAR EXTEND Gram
`Id { name=name; recarg_like=recarg_like;
notation_scope=f notation_scope;
implicit_status = NotImplicit}) items }
- | "["; items = LIST1 argument_spec; "]"; sc = OPT scope ->
+ | "["; 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
@@ -868,7 +869,7 @@ GRAMMAR EXTEND Gram
`Id { name=name; recarg_like=recarg_like;
notation_scope=f notation_scope;
implicit_status = Implicit}) items }
- | "{"; items = LIST1 argument_spec; "}"; sc = OPT scope ->
+ | "{"; 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
@@ -1136,11 +1137,8 @@ GRAMMAR EXTEND Gram
positive_search_mark:
[ [ "-" -> { false } | -> { true } ] ]
;
- scope:
- [ [ "%"; key = IDENT -> { key } ] ]
- ;
searchabout_query:
- [ [ b = positive_search_mark; s = ne_string; sc = OPT scope ->
+ [ [ b = positive_search_mark; s = ne_string; sc = OPT scope_delimiter ->
{ (b, SearchString (s,sc)) }
| b = positive_search_mark; p = constr_pattern ->
{ (b, SearchSubPattern p) }
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-05 13:06:45 +0000