diff options
79 files changed, 532 insertions, 568 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 2947bfb700..45597851ef 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -229,7 +229,6 @@ windows64: <<: *windows-template variables: ARCH: "64" - allow_failure: true windows32: <<: *windows-template @@ -237,7 +236,6 @@ windows32: ARCH: "32" except: - /^pr-.*$/ - allow_failure: true pkg:opam: stage: test diff --git a/appveyor.yml b/appveyor.yml index c9c6bc0684..7420856214 100644 --- a/appveyor.yml +++ b/appveyor.yml @@ -2,8 +2,7 @@ version: '{branch}~{build}' clone_depth: 10 cache: - - C:\cygwin64 -> dev\ci\appveyor.bat - - C:\cygwin64\home\appveyor\.opam -> dev\ci\appveyor.sh + - C:\cygwin64 -> dev\ci\appveyor.bat, dev\ci\appveyor.sh platform: - x64 diff --git a/coqpp/coqpp_main.ml b/coqpp/coqpp_main.ml index d52bd39d72..8d728b5b51 100644 --- a/coqpp/coqpp_main.ml +++ b/coqpp/coqpp_main.ml @@ -146,16 +146,16 @@ let print_local fmt ext = fprintf fmt "in@ " let print_position fmt pos = match pos with -| First -> fprintf fmt "Extend.First" -| Last -> fprintf fmt "Extend.Last" -| Before s -> fprintf fmt "Extend.Before@ \"%s\"" s -| After s -> fprintf fmt "Extend.After@ \"%s\"" s -| Level s -> fprintf fmt "Extend.Level@ \"%s\"" s +| First -> fprintf fmt "Gramlib.Gramext.First" +| Last -> fprintf fmt "Gramlib.Gramext.Last" +| Before s -> fprintf fmt "Gramlib.Gramext.Before@ \"%s\"" s +| After s -> fprintf fmt "Gramlib.Gramext.After@ \"%s\"" s +| Level s -> fprintf fmt "Gramlib.Gramext.Level@ \"%s\"" s let print_assoc fmt = function -| LeftA -> fprintf fmt "Extend.LeftA" -| RightA -> fprintf fmt "Extend.RightA" -| NonA -> fprintf fmt "Extend.NonA" +| LeftA -> fprintf fmt "Gramlib.Gramext.LeftA" +| RightA -> fprintf fmt "Gramlib.Gramext.RightA" +| NonA -> fprintf fmt "Gramlib.Gramext.NonA" let is_token s = match string_split s with | [s] -> is_uident s diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh index d0b5f4be47..b202635714 100755 --- a/dev/build/windows/makecoq_mingw.sh +++ b/dev/build/windows/makecoq_mingw.sh @@ -1905,6 +1905,9 @@ function make_addon_quickchick { function make_addons { # Note: ':' is the empty command, which does not produce any output : > "/build/filelists/addon_dependencies.nsh" + : > "/build/filelists/addon_strings.nsh" + : > "/build/filelists/addon_descriptions.nsh" + : > "/build/filelists/addon_sections.nsh" for addon in $COQ_ADDONS; do "make_addon_$addon" diff --git a/dev/ci/appveyor.sh b/dev/ci/appveyor.sh index abeb039c0e..cda369fb1b 100644 --- a/dev/ci/appveyor.sh +++ b/dev/ci/appveyor.sh @@ -2,14 +2,15 @@ set -e -x -APPVEYOR_OPAM_SWITCH=4.07.0+mingw64c +APPVEYOR_OPAM_VARIANT=ocaml-variants.4.07.1+mingw64c -wget https://github.com/fdopen/opam-repository-mingw/releases/download/0.0.0.1/opam64.tar.xz +wget https://github.com/fdopen/opam-repository-mingw/releases/download/0.0.0.2/opam64.tar.xz -O opam64.tar.xz tar -xf opam64.tar.xz bash opam64/install.sh -opam init -a mingw https://github.com/fdopen/opam-repository-mingw.git --comp $APPVEYOR_OPAM_SWITCH --switch $APPVEYOR_OPAM_SWITCH -eval "$(opam config env)" +opam init default -a -y "https://github.com/fdopen/opam-repository-mingw.git#opam2" -c $APPVEYOR_OPAM_VARIANT --disable-sandboxing +eval "$(opam env)" opam install -y num ocamlfind ounit +# Full regular Coq Build cd "$APPVEYOR_BUILD_FOLDER" && ./configure -local && make && make byte && make -C test-suite all INTERACTIVE= # && make validate diff --git a/dev/ci/gitlab.bat b/dev/ci/gitlab.bat index 918d289ae2..386a3de204 100755 --- a/dev/ci/gitlab.bat +++ b/dev/ci/gitlab.bat @@ -39,6 +39,10 @@ SET PATH=%PATH%;C:\Program Files\7-Zip\;C:\Program Files\Microsoft SDKs\Windows\ IF "%WINDOWS%" == "enabled_all_addons" (
SET EXTRA_ADDONS=^
+ -addon=bignums ^
+ -addon=equations ^
+ -addon=ltac2 ^
+ -addon=mtac2 ^
-addon=mathcomp ^
-addon=menhir ^
-addon=menhirlib ^
@@ -56,10 +60,6 @@ IF "%WINDOWS%" == "enabled_all_addons" ( call %CI_PROJECT_DIR%\dev\build\windows\MakeCoq_MinGW.bat -threads=1 ^
-arch=%ARCH% -installer=Y -coqver=%CI_PROJECT_DIR_CFMT% ^
-destcyg=%CYGROOT% -destcoq=%DESTCOQ% -cygcache=%CYGCACHE% ^
- -addon=bignums ^
- -addon=equations ^
- -addon=ltac2 ^
- -addon=mtac2 ^
%EXTRA_ADDONS% ^
-make=N ^
-setup %CI_PROJECT_DIR%\%SETUP% || GOTO ErrorCopyLogFilesAndExit
diff --git a/dev/ci/user-overlays/09102-ejgallego-ltac+remove_aliases.sh b/dev/ci/user-overlays/09102-ejgallego-ltac+remove_aliases.sh new file mode 100644 index 0000000000..2df8affd14 --- /dev/null +++ b/dev/ci/user-overlays/09102-ejgallego-ltac+remove_aliases.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "9102" ] || [ "$CI_BRANCH" = "ltac+remove_aliases" ]; then + + elpi_CI_REF=ltac+remove_aliases + elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi + +fi diff --git a/doc/sphinx/addendum/implicit-coercions.rst b/doc/sphinx/addendum/implicit-coercions.rst index c8fb4bd00e..789890eab5 100644 --- a/doc/sphinx/addendum/implicit-coercions.rst +++ b/doc/sphinx/addendum/implicit-coercions.rst @@ -285,19 +285,21 @@ Activating the Printing of Coercions Classes as Records ------------------ +.. index:: :> (coercion) + We allow the definition of *Structures with Inheritance* (or classes as records) by extending the existing :cmd:`Record` macro. Its new syntax is: .. cmdv:: Record {? >} @ident {? @binders} : @sort := {? @ident} { {+; @ident :{? >} @term } } - The first identifier `ident` is the name of the defined record and - `sort` is its type. The optional identifier after ``:=`` is the name - of the constuctor (it will be ``Build_``\ `ident` if not given). - The other identifiers are the names of the fields, and the `term` + The first identifier :token:`ident` is the name of the defined record and + :token:`sort` is its type. The optional identifier after ``:=`` is the name + of the constuctor (it will be :n:`Build_@ident` if not given). + The other identifiers are the names of the fields, and :token:`term` are their respective types. If ``:>`` is used instead of ``:`` in the declaration of a field, then the name of this field is automatically declared as a coercion from the record name to the class of this - field type. Remark that the fields always verify the uniform + field type. Note that the fields always verify the uniform inheritance condition. If the optional ``>`` is given before the record name, then the constructor name is automatically declared as a coercion from the class of the last field type to the record name diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst index cc8870e2e4..e153c7cbe2 100644 --- a/doc/sphinx/addendum/program.rst +++ b/doc/sphinx/addendum/program.rst @@ -102,7 +102,7 @@ Syntactic control over equalities To give more control over the generation of equalities, the type checker will fall back directly to |Coq|’s usual typing of dependent -pattern matching if a return or in clause is specified. Likewise, the +pattern matching if a ``return`` or ``in`` clause is specified. Likewise, the if construct is not treated specially by |Program| so boolean tests in the code are not automatically reflected in the obligations. One can use the :g:`dec` combinator to get the correct hypotheses as in: @@ -118,8 +118,9 @@ use the :g:`dec` combinator to get the correct hypotheses as in: else S (pred n). The :g:`let` tupling construct :g:`let (x1, ..., xn) := t in b` does not -produce an equality, contrary to the let pattern construct :g:`let ’(x1, -..., xn) := t in b`. Also, :g:`term :>` explicitly asks the system to +produce an equality, contrary to the let pattern construct +:g:`let '(x1,..., xn) := t in b`. +Also, :g:`term :>` explicitly asks the system to coerce term to its support type. It can be useful in notations, for example: diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst index 15a55d9e72..98dfcb2373 100644 --- a/doc/sphinx/addendum/type-classes.rst +++ b/doc/sphinx/addendum/type-classes.rst @@ -228,6 +228,8 @@ mechanism if available, as shown in the example. Substructures ~~~~~~~~~~~~~ +.. index:: :> (substructure) + Substructures are components of a class which are instances of a class themselves. They often arise when using classes for logical properties, e.g.: @@ -260,6 +262,12 @@ preorder can be used instead. This is very similar to the coercion mechanism of ``Structure`` declarations. The implementation simply declares each projection as an instance. +.. warn:: Ignored instance declaration for “@ident”: “@term” is not a class + + Using this ``:>`` syntax with a right-hand-side that is not itself a Class + has no effect (apart from emitting this warning). In particular, is does not + declare a coercion. + One can also declare existing objects or structure projections using the Existing Instance command to achieve the same effect. diff --git a/doc/sphinx/language/coq-library.rst b/doc/sphinx/language/coq-library.rst index 85474a3e98..10650af1d1 100644 --- a/doc/sphinx/language/coq-library.rst +++ b/doc/sphinx/language/coq-library.rst @@ -97,8 +97,8 @@ Logic The basic library of |Coq| comes with the definitions of standard (intuitionistic) logical connectives (they are defined as inductive constructions). They are equipped with an appealing syntax enriching the -subclass `form` of the syntactic class `term`. The syntax of `form` -is shown below: +subclass :token:`form` of the syntactic class :token:`term`. The syntax of +:token:`form` is shown below: .. /!\ Please keep the blanks in the lines below, experimentally they produce a nice last column. Or even better, find a proper way to do this! diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 65df89da6c..1c53f5981d 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -1380,147 +1380,147 @@ Numeral notations .. cmd:: Numeral Notation @ident__1 @ident__2 @ident__3 : @scope. :name: Numeral Notation - This command allows the user to customize the way numeral literals - are parsed and printed. + This command allows the user to customize the way numeral literals + are parsed and printed. - The token :n:`@ident__1` should be the name of an inductive type, - while :n:`@ident__2` and :n:`@ident__3` should be the names of the - parsing and printing functions, respectively. The parsing function - :n:`@ident__2` should have one of the following types: + The token :n:`@ident__1` should be the name of an inductive type, + while :n:`@ident__2` and :n:`@ident__3` should be the names of the + parsing and printing functions, respectively. The parsing function + :n:`@ident__2` should have one of the following types: - * :n:`Decimal.int -> @ident__1` - * :n:`Decimal.int -> option @ident__1` - * :n:`Decimal.uint -> @ident__1` - * :n:`Decimal.uint -> option @ident__1` - * :n:`Z -> @ident__1` - * :n:`Z -> option @ident__1` + * :n:`Decimal.int -> @ident__1` + * :n:`Decimal.int -> option @ident__1` + * :n:`Decimal.uint -> @ident__1` + * :n:`Decimal.uint -> option @ident__1` + * :n:`Z -> @ident__1` + * :n:`Z -> option @ident__1` - And the printing function :n:`@ident__3` should have one of the - following types: + And the printing function :n:`@ident__3` should have one of the + following types: - * :n:`@ident__1 -> Decimal.int` - * :n:`@ident__1 -> option Decimal.int` - * :n:`@ident__1 -> Decimal.uint` - * :n:`@ident__1 -> option Decimal.uint` - * :n:`@ident__1 -> Z` - * :n:`@ident__1 -> option Z` + * :n:`@ident__1 -> Decimal.int` + * :n:`@ident__1 -> option Decimal.int` + * :n:`@ident__1 -> Decimal.uint` + * :n:`@ident__1 -> option Decimal.uint` + * :n:`@ident__1 -> Z` + * :n:`@ident__1 -> option Z` - When parsing, the application of the parsing function - :n:`@ident__2` to the number will be fully reduced, and universes - of the resulting term will be refreshed. + When parsing, the application of the parsing function + :n:`@ident__2` to the number will be fully reduced, and universes + of the resulting term will be refreshed. - .. cmdv:: Numeral Notation @ident__1 @ident__2 @ident__3 : @scope (warning after @num). + .. cmdv:: Numeral Notation @ident__1 @ident__2 @ident__3 : @scope (warning after @num). - When a literal larger than :token:`num` is parsed, a warning - message about possible stack overflow, resulting from evaluating - :n:`@ident__2`, will be displayed. + When a literal larger than :token:`num` is parsed, a warning + message about possible stack overflow, resulting from evaluating + :n:`@ident__2`, will be displayed. - .. cmdv:: Numeral Notation @ident__1 @ident__2 @ident__3 : @scope (abstract after @num). + .. cmdv:: Numeral Notation @ident__1 @ident__2 @ident__3 : @scope (abstract after @num). - When a literal :g:`m` larger than :token:`num` is parsed, the - result will be :n:`(@ident__2 m)`, without reduction of this - application to a normal form. Here :g:`m` will be a - :g:`Decimal.int` or :g:`Decimal.uint` or :g:`Z`, depending on the - type of the parsing function :n:`@ident__2`. This allows for a - more compact representation of literals in types such as :g:`nat`, - and limits parse failures due to stack overflow. Note that a - warning will be emitted when an integer larger than :token:`num` - is parsed. Note that :n:`(abstract after @num)` has no effect - when :n:`@ident__2` lands in an :g:`option` type. + When a literal :g:`m` larger than :token:`num` is parsed, the + result will be :n:`(@ident__2 m)`, without reduction of this + application to a normal form. Here :g:`m` will be a + :g:`Decimal.int` or :g:`Decimal.uint` or :g:`Z`, depending on the + type of the parsing function :n:`@ident__2`. This allows for a + more compact representation of literals in types such as :g:`nat`, + and limits parse failures due to stack overflow. Note that a + warning will be emitted when an integer larger than :token:`num` + is parsed. Note that :n:`(abstract after @num)` has no effect + when :n:`@ident__2` lands in an :g:`option` type. - .. exn:: Cannot interpret this number as a value of type @type + .. exn:: Cannot interpret this number as a value of type @type - The numeral notation registered for :token:`type` does not support - the given numeral. This error is given when the interpretation - function returns :g:`None`, or if the interpretation is registered - for only non-negative integers, and the given numeral is negative. + The numeral notation registered for :token:`type` does not support + the given numeral. This error is given when the interpretation + function returns :g:`None`, or if the interpretation is registered + for only non-negative integers, and the given numeral is negative. - .. exn:: @ident should go from Decimal.int to @type or (option @type). Instead of Decimal.int, the types Decimal.uint or Z could be used{? (require BinNums first)}. + .. exn:: @ident should go from Decimal.int to @type or (option @type). Instead of Decimal.int, the types Decimal.uint or Z could be used{? (require BinNums first)}. - The parsing function given to the :cmd:`Numeral Notation` - vernacular is not of the right type. + The parsing function given to the :cmd:`Numeral Notation` + vernacular is not of the right type. - .. exn:: @ident should go from @type to Decimal.int or (option Decimal.int). Instead of Decimal.int, the types Decimal.uint or Z could be used{? (require BinNums first)}. + .. exn:: @ident should go from @type to Decimal.int or (option Decimal.int). Instead of Decimal.int, the types Decimal.uint or Z could be used{? (require BinNums first)}. - The printing function given to the :cmd:`Numeral Notation` - vernacular is not of the right type. + The printing function given to the :cmd:`Numeral Notation` + vernacular is not of the right type. - .. exn:: @type is not an inductive type. + .. exn:: @type is not an inductive type. - Numeral notations can only be declared for inductive types with no - arguments. + Numeral notations can only be declared for inductive types with no + arguments. - .. exn:: Unexpected term @term while parsing a numeral notation. + .. exn:: Unexpected term @term while parsing a numeral notation. - Parsing functions must always return ground terms, made up of - applications of constructors and inductive types. Parsing - functions may not return terms containing axioms, bare - (co)fixpoints, lambdas, etc. + Parsing functions must always return ground terms, made up of + applications of constructors and inductive types. Parsing + functions may not return terms containing axioms, bare + (co)fixpoints, lambdas, etc. - .. exn:: Unexpected non-option term @term while parsing a numeral notation. + .. exn:: Unexpected non-option term @term while parsing a numeral notation. - Parsing functions expected to return an :g:`option` must always - return a concrete :g:`Some` or :g:`None` when applied to a - concrete numeral expressed as a decimal. They may not return - opaque constants. + Parsing functions expected to return an :g:`option` must always + return a concrete :g:`Some` or :g:`None` when applied to a + concrete numeral expressed as a decimal. They may not return + opaque constants. - .. exn:: Cannot interpret in @scope because @ident could not be found in the current environment. + .. exn:: Cannot interpret in @scope because @ident could not be found in the current environment. - The inductive type used to register the numeral notation is no - longer available in the environment. Most likely, this is because - the numeral notation was declared inside a functor for an - inductive type inside the functor. This use case is not currently - supported. + The inductive type used to register the numeral notation is no + longer available in the environment. Most likely, this is because + the numeral notation was declared inside a functor for an + inductive type inside the functor. This use case is not currently + supported. - Alternatively, you might be trying to use a primitive token - notation from a plugin which forgot to specify which module you - must :g:`Require` for access to that notation. + Alternatively, you might be trying to use a primitive token + notation from a plugin which forgot to specify which module you + must :g:`Require` for access to that notation. - .. exn:: Syntax error: [prim:reference] expected after 'Notation' (in [vernac:command]). + .. exn:: Syntax error: [prim:reference] expected after 'Notation' (in [vernac:command]). - The type passed to :cmd:`Numeral Notation` must be a single - identifier. + The type passed to :cmd:`Numeral Notation` must be a single + identifier. - .. exn:: Syntax error: [prim:reference] expected after [prim:reference] (in [vernac:command]). + .. exn:: Syntax error: [prim:reference] expected after [prim:reference] (in [vernac:command]). - Both functions passed to :cmd:`Numeral Notation` must be single - identifiers. + Both functions passed to :cmd:`Numeral Notation` must be single + identifiers. - .. exn:: The reference @ident was not found in the current environment. + .. exn:: The reference @ident was not found in the current environment. - Identifiers passed to :cmd:`Numeral Notation` must exist in the - global environment. + Identifiers passed to :cmd:`Numeral Notation` must exist in the + global environment. - .. exn:: @ident is bound to a notation that does not denote a reference. + .. exn:: @ident is bound to a notation that does not denote a reference. - Identifiers passed to :cmd:`Numeral Notation` must be global - references, or notations which denote to single identifiers. + Identifiers passed to :cmd:`Numeral Notation` must be global + references, or notations which denote to single identifiers. - .. warn:: Stack overflow or segmentation fault happens when working with large numbers in @type (threshold may vary depending on your system limits and on the command executed). + .. warn:: Stack overflow or segmentation fault happens when working with large numbers in @type (threshold may vary depending on your system limits and on the command executed). - When a :cmd:`Numeral Notation` is registered in the current scope - with :n:`(warning after @num)`, this warning is emitted when - parsing a numeral greater than or equal to :token:`num`. + When a :cmd:`Numeral Notation` is registered in the current scope + with :n:`(warning after @num)`, this warning is emitted when + parsing a numeral greater than or equal to :token:`num`. - .. warn:: To avoid stack overflow, large numbers in @type are interpreted as applications of @ident__2. + .. warn:: To avoid stack overflow, large numbers in @type are interpreted as applications of @ident__2. - When a :cmd:`Numeral Notation` is registered in the current scope - with :n:`(abstract after @num)`, this warning is emitted when - parsing a numeral greater than or equal to :token:`num`. - Typically, this indicates that the fully computed representation - of numerals can be so large that non-tail-recursive OCaml - functions run out of stack space when trying to walk them. + When a :cmd:`Numeral Notation` is registered in the current scope + with :n:`(abstract after @num)`, this warning is emitted when + parsing a numeral greater than or equal to :token:`num`. + Typically, this indicates that the fully computed representation + of numerals can be so large that non-tail-recursive OCaml + functions run out of stack space when trying to walk them. - For example + For example - .. coqtop:: all + .. coqtop:: all - Check 90000. + Check 90000. - .. warn:: The 'abstract after' directive has no effect when the parsing function (@ident__2) targets an option type. + .. warn:: The 'abstract after' directive has no effect when the parsing function (@ident__2) targets an option type. - As noted above, the :n:`(abstract after @num)` directive has no - effect when :n:`@ident__2` lands in an :g:`option` type. + As noted above, the :n:`(abstract after @num)` directive has no + effect when :n:`@ident__2` lands in an :g:`option` type. .. _TacticNotation: diff --git a/engine/namegen.ml b/engine/namegen.ml index 0f346edd3e..a67ff6965b 100644 --- a/engine/namegen.ml +++ b/engine/namegen.ml @@ -208,23 +208,16 @@ let it_mkLambda_or_LetIn_name env sigma b hyps = (* Introduce a mode where auto-generated names are mangled to test dependence of scripts on auto-generated names *) -let mangle_names = ref false - -let () = Goptions.( - declare_bool_option - { optdepr = false; - optname = "mangle auto-generated names"; - optkey = ["Mangle";"Names"]; - optread = (fun () -> !mangle_names); - optwrite = (:=) mangle_names; }) +let get_mangle_names = + Goptions.declare_bool_option_and_ref + ~depr:false + ~name:"mangle auto-generated names" + ~key:["Mangle";"Names"] + ~value:false let mangle_names_prefix = ref (Id.of_string "_0") -let set_prefix x = mangle_names_prefix := forget_subscript x -let set_mangle_names_mode x = begin - set_prefix x; - mangle_names := true - end +let set_prefix x = mangle_names_prefix := forget_subscript x let () = Goptions.( declare_string_option @@ -238,7 +231,7 @@ let () = Goptions.( with CErrors.UserError _ -> CErrors.user_err Pp.(str ("Not a valid identifier: \"" ^ x ^ "\"."))) end }) -let mangle_id id = if !mangle_names then !mangle_names_prefix else id +let mangle_id id = if get_mangle_names () then !mangle_names_prefix else id (* Looks for next "good" name by lifting subscript *) diff --git a/engine/namegen.mli b/engine/namegen.mli index a53c3a0d1f..3722cbed24 100644 --- a/engine/namegen.mli +++ b/engine/namegen.mli @@ -125,7 +125,3 @@ val rename_bound_vars_as_displayed : val compute_displayed_name_in_gen : (evar_map -> int -> 'a -> bool) -> evar_map -> Id.Set.t -> Name.t -> 'a -> Name.t * Id.Set.t - -val set_mangle_names_mode : Id.t -> unit -(** Turn on mangled names mode and with the given prefix. - @raise UserError if the argument is invalid as an identifier. *) diff --git a/engine/univMinim.ml b/engine/univMinim.ml index 68c2724f26..e20055b133 100644 --- a/engine/univMinim.ml +++ b/engine/univMinim.ml @@ -12,17 +12,12 @@ open Univ open UnivSubst (* To disallow minimization to Set *) -let set_minimization = ref true -let is_set_minimization () = !set_minimization - -let () = - Goptions.(declare_bool_option - { optdepr = false; - optname = "minimization to Set"; - optkey = ["Universe";"Minimization";"ToSet"]; - optread = is_set_minimization; - optwrite = (:=) set_minimization }) - +let get_set_minimization = + Goptions.declare_bool_option_and_ref + ~depr:false + ~name:"minimization to Set" + ~key:["Universe";"Minimization";"ToSet"] + ~value:true (** Simplification *) @@ -278,7 +273,7 @@ let normalize_context_set g ctx us algs weak = let smallles, csts = Constraint.partition (fun (l,d,r) -> d == Le && Level.is_small l) csts in - let smallles = if is_set_minimization () + let smallles = if get_set_minimization () then Constraint.filter (fun (l,d,r) -> LSet.mem r ctx) smallles else Constraint.empty in diff --git a/gramlib/gramext.ml b/gramlib/gramext.ml index 43a70ca13b..c35c4bd18e 100644 --- a/gramlib/gramext.ml +++ b/gramlib/gramext.ml @@ -55,8 +55,6 @@ type position = | Like of string | Level of string -let warning_verbose = ref true - let rec derive_eps = function Slist0 _ -> true @@ -96,7 +94,7 @@ let is_before s1 s2 = | Stoken _, _ -> true | _ -> false -let insert_tree entry_name gsymbols action tree = +let insert_tree ~warning entry_name gsymbols action tree = let rec insert symbols tree = match symbols with s :: sl -> insert_in_tree s sl tree @@ -105,14 +103,16 @@ let insert_tree entry_name gsymbols action tree = Node {node = s; son = son; brother = bro} -> Node {node = s; son = son; brother = insert [] bro} | LocAct (old_action, action_list) -> - if !warning_verbose then - begin - eprintf "<W> Grammar extension: "; - if entry_name <> "" then eprintf "in [%s], " entry_name; - eprintf "some rule has been masked\n"; - flush stderr - end; - LocAct (action, old_action :: action_list) + begin match warning with + | None -> () + | Some warn_fn -> + let msg = + "<W> Grammar extension: " ^ + (if entry_name <> "" then "" else "in ["^entry_name^"%s], ") ^ + "some rule has been masked" in + warn_fn msg + end; + LocAct (action, old_action :: action_list) | DeadEnd -> LocAct (action, []) and insert_in_tree s sl tree = match try_insert s sl tree with @@ -141,10 +141,10 @@ let insert_tree entry_name gsymbols action tree = in insert gsymbols tree -let srules rl = +let srules ~warning rl = let t = List.fold_left - (fun tree (symbols, action) -> insert_tree "" symbols action tree) + (fun tree (symbols, action) -> insert_tree ~warning "" symbols action tree) DeadEnd rl in Stree t @@ -175,15 +175,15 @@ and token_exists_in_symbol f = | Stree t -> token_exists_in_tree f t | Snterm _ | Snterml (_, _) | Snext | Sself -> false -let insert_level entry_name e1 symbols action slev = +let insert_level ~warning entry_name e1 symbols action slev = match e1 with true -> {assoc = slev.assoc; lname = slev.lname; - lsuffix = insert_tree entry_name symbols action slev.lsuffix; + lsuffix = insert_tree ~warning entry_name symbols action slev.lsuffix; lprefix = slev.lprefix} | false -> {assoc = slev.assoc; lname = slev.lname; lsuffix = slev.lsuffix; - lprefix = insert_tree entry_name symbols action slev.lprefix} + lprefix = insert_tree ~warning entry_name symbols action slev.lprefix} let empty_lev lname assoc = let assoc = @@ -193,27 +193,33 @@ let empty_lev lname assoc = in {assoc = assoc; lname = lname; lsuffix = DeadEnd; lprefix = DeadEnd} -let change_lev lev n lname assoc = +let change_lev ~warning lev n lname assoc = let a = match assoc with None -> lev.assoc | Some a -> - if a <> lev.assoc && !warning_verbose then - begin - eprintf "<W> Changing associativity of level \"%s\"\n" n; - flush stderr - end; + if a <> lev.assoc then + begin + match warning with + | None -> () + | Some warn_fn -> + warn_fn ("<W> Changing associativity of level \""^n^"\"") + end; a in begin match lname with Some n -> - if lname <> lev.lname && !warning_verbose then - begin eprintf "<W> Level label \"%s\" ignored\n" n; flush stderr end + if lname <> lev.lname then + begin match warning with + | None -> () + | Some warn_fn -> + warn_fn ("<W> Level label \""^n^"\" ignored") + end; | None -> () end; {assoc = a; lname = lev.lname; lsuffix = lev.lsuffix; lprefix = lev.lprefix} -let get_level entry position levs = +let get_level ~warning entry position levs = match position with Some First -> [], empty_lev, levs | Some Last -> levs, empty_lev, [] @@ -226,7 +232,7 @@ let get_level entry position levs = flush stderr; failwith "Grammar.extend" | lev :: levs -> - if is_level_labelled n lev then [], change_lev lev n, levs + if is_level_labelled n lev then [], change_lev ~warning lev n, levs else let (levs1, rlev, levs2) = get levs in lev :: levs1, rlev, levs2 in @@ -268,14 +274,14 @@ let get_level entry position levs = flush stderr; failwith "Grammar.extend" | lev :: levs -> - if token_exists_in_level f lev then [], change_lev lev n, levs + if token_exists_in_level f lev then [], change_lev ~warning lev n, levs else let (levs1, rlev, levs2) = get levs in lev :: levs1, rlev, levs2 in get levs | None -> match levs with - lev :: levs -> [], change_lev lev "<top>", levs + lev :: levs -> [], change_lev ~warning lev "<top>", levs | [] -> [], empty_lev, [] let rec check_gram entry = @@ -347,7 +353,7 @@ let insert_tokens gram symbols = in List.iter insert symbols -let levels_of_rules entry position rules = +let levels_of_rules ~warning entry position rules = let elev = match entry.edesc with Dlevels elev -> elev @@ -358,7 +364,7 @@ let levels_of_rules entry position rules = in if rules = [] then elev else - let (levs1, make_lev, levs2) = get_level entry position elev in + let (levs1, make_lev, levs2) = get_level ~warning entry position elev in let (levs, _) = List.fold_left (fun (levs, make_lev) (lname, assoc, level) -> @@ -370,7 +376,7 @@ let levels_of_rules entry position rules = List.iter (check_gram entry) symbols; let (e1, symbols) = get_initial entry symbols in insert_tokens entry.egram symbols; - insert_level entry.ename e1 symbols action lev) + insert_level ~warning entry.ename e1 symbols action lev) lev level in lev :: levs, empty_lev) diff --git a/gramlib/gramext.mli b/gramlib/gramext.mli index 8361e21645..ecb95ec61b 100644 --- a/gramlib/gramext.mli +++ b/gramlib/gramext.mli @@ -53,15 +53,14 @@ type position = | Like of string | Level of string -val levels_of_rules : +val levels_of_rules : warning:(string -> unit) option -> 'te g_entry -> position option -> (string option * g_assoc option * ('te g_symbol list * g_action) list) list -> 'te g_level list -val srules : ('te g_symbol list * g_action) list -> 'te g_symbol + +val srules : warning:(string -> unit) option -> ('te g_symbol list * g_action) list -> 'te g_symbol val eq_symbol : 'a g_symbol -> 'a g_symbol -> bool val delete_rule_in_level_list : 'te g_entry -> 'te g_symbol list -> 'te g_level list -> 'te g_level list - -val warning_verbose : bool ref diff --git a/gramlib/grammar.ml b/gramlib/grammar.ml index dfce26a33a..285c14ec62 100644 --- a/gramlib/grammar.ml +++ b/gramlib/grammar.ml @@ -755,9 +755,9 @@ let init_entry_functions entry = let f = continue_parser_of_entry entry in entry.econtinue <- f; f lev bp a strm) -let extend_entry entry position rules = +let extend_entry ~warning entry position rules = try - let elev = Gramext.levels_of_rules entry position rules in + let elev = Gramext.levels_of_rules ~warning entry position rules in entry.edesc <- Dlevels elev; init_entry_functions entry with Plexing.Error s -> Printf.eprintf "Lexer initialization error:\n- %s\n" s; @@ -841,8 +841,6 @@ let clear_entry e = Dlevels _ -> e.edesc <- Dlevels [] | Dparser _ -> () -let gram_reinit g glexer = Hashtbl.clear g.gtokens; g.glexer <- glexer - (* Functorial interface *) module type GLexerType = sig type te val lexer : te Plexing.lexer end @@ -881,7 +879,7 @@ module type S = val s_self : ('self, 'self) ty_symbol val s_next : ('self, 'self) ty_symbol val s_token : Plexing.pattern -> ('self, string) ty_symbol - val s_rules : 'a ty_production list -> ('self, 'a) ty_symbol + val s_rules : warning:(string -> unit) option -> 'a ty_production list -> ('self, 'a) ty_symbol val r_stop : ('self, 'r, 'r) ty_rule val r_next : ('self, 'a, 'r) ty_rule -> ('self, 'b) ty_symbol -> @@ -889,10 +887,9 @@ module type S = val production : ('a, 'f, Ploc.t -> 'a) ty_rule * 'f -> 'a ty_production module Unsafe : sig - val gram_reinit : te Plexing.lexer -> unit val clear_entry : 'a Entry.e -> unit end - val safe_extend : + val safe_extend : warning:(string -> unit) option -> 'a Entry.e -> Gramext.position option -> (string option * Gramext.g_assoc option * 'a ty_production list) list -> @@ -945,7 +942,7 @@ module GMake (L : GLexerType) = let s_self = Sself let s_next = Snext let s_token tok = Stoken tok - let s_rules (t : Obj.t ty_production list) = Gramext.srules (Obj.magic t) + let s_rules ~warning (t : Obj.t ty_production list) = Gramext.srules ~warning (Obj.magic t) let r_stop = [] let r_next r s = r @ [s] let production @@ -953,15 +950,12 @@ module GMake (L : GLexerType) = Obj.magic p module Unsafe = struct - let gram_reinit = gram_reinit gram let clear_entry = clear_entry end - let extend = extend_entry - let safe_extend e pos + let safe_extend ~warning e pos (r : (string option * Gramext.g_assoc option * Obj.t ty_production list) list) = - extend e pos (Obj.magic r) - let delete_rule e r = delete_rule (Entry.obj e) r - let safe_delete_rule = delete_rule + extend_entry ~warning e pos (Obj.magic r) + let safe_delete_rule e r = delete_rule (Entry.obj e) r end diff --git a/gramlib/grammar.mli b/gramlib/grammar.mli index 1e14e557bc..0c585a7c0d 100644 --- a/gramlib/grammar.mli +++ b/gramlib/grammar.mli @@ -53,7 +53,7 @@ module type S = val s_self : ('self, 'self) ty_symbol val s_next : ('self, 'self) ty_symbol val s_token : Plexing.pattern -> ('self, string) ty_symbol - val s_rules : 'a ty_production list -> ('self, 'a) ty_symbol + val s_rules : warning:(string -> unit) option -> 'a ty_production list -> ('self, 'a) ty_symbol val r_stop : ('self, 'r, 'r) ty_rule val r_next : ('self, 'a, 'r) ty_rule -> ('self, 'b) ty_symbol -> @@ -62,10 +62,9 @@ module type S = module Unsafe : sig - val gram_reinit : te Plexing.lexer -> unit val clear_entry : 'a Entry.e -> unit end - val safe_extend : + val safe_extend : warning:(string -> unit) option -> 'a Entry.e -> Gramext.position option -> (string option * Gramext.g_assoc option * 'a ty_production list) list -> diff --git a/ide/coqide_WIN32.ml.in b/ide/coqide_WIN32.ml.in index 8c4649fc39..0793a1cc1c 100644 --- a/ide/coqide_WIN32.ml.in +++ b/ide/coqide_WIN32.ml.in @@ -37,9 +37,8 @@ let reroute_stdout_stderr () = Unix.dup2 out_descr Unix.stdout; Unix.dup2 out_descr Unix.stderr -(* We also provide specific kill and interrupt functions. *) +(* We also provide a specific interrupt function. *) -external win32_kill : int -> unit = "win32_kill" external win32_interrupt : int -> unit = "win32_interrupt" let () = Coq.gio_channel_of_descr_socket := Glib.Io.channel_of_descr_socket; diff --git a/ide/ide_win32_stubs.c b/ide/ide_win32_stubs.c index c09bf37dee..f430c9f2b6 100644 --- a/ide/ide_win32_stubs.c +++ b/ide/ide_win32_stubs.c @@ -4,22 +4,6 @@ #include <caml/memory.h> #include <windows.h> -/* Win32 emulation of kill -9 */ - -/* The pid returned by Unix.create_process is actually a pseudo-pid, - made via a cast of the obtained HANDLE, (cf. win32unix/createprocess.c - in the sources of ocaml). Since we're still in the caller process, - we simply cast back to get an handle... - The 0 is the exit code we want for the terminated process. -*/ - -CAMLprim value win32_kill(value pseudopid) { - CAMLparam1(pseudopid); - TerminateProcess((HANDLE)(Long_val(pseudopid)), 0); - CAMLreturn(Val_unit); -} - - /* Win32 emulation of a kill -2 (SIGINT) */ /* This code rely of the fact that coqide is now without initial console. diff --git a/ide/idetop.ml b/ide/idetop.ml index 8cb02190e6..a2b85041e8 100644 --- a/ide/idetop.ml +++ b/ide/idetop.ml @@ -537,5 +537,5 @@ let islave_init ~opts extra_args = let () = let open Coqtop in - let custom = { init = islave_init; run = loop; } in + let custom = { init = islave_init; run = loop; opts = Coqargs.default_opts } in start_coq custom diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml index 07ed7825ff..3a4969a3ee 100644 --- a/interp/constrexpr_ops.ml +++ b/interp/constrexpr_ops.ml @@ -604,15 +604,6 @@ let rec coerce_to_cases_pattern_expr c = CAst.map_with_loc (fun ?loc -> function CErrors.user_err ?loc ~hdr:"coerce_to_cases_pattern_expr" (str "This expression should be coercible to a pattern.")) c -let asymmetric_patterns = ref (false) -let () = Goptions.(declare_bool_option { - optdepr = false; - optname = "no parameters in constructors"; - optkey = ["Asymmetric";"Patterns"]; - optread = (fun () -> !asymmetric_patterns); - optwrite = (fun a -> asymmetric_patterns:=a); -}) - (** Local universe and constraint declarations. *) let interp_univ_constraints env evd cstrs = diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli index 9e83bde8b2..7f14eb4583 100644 --- a/interp/constrexpr_ops.mli +++ b/interp/constrexpr_ops.mli @@ -127,9 +127,6 @@ val patntn_loc : ?loc:Loc.t -> cases_pattern_notation_substitution -> notation - (** For cases pattern parsing errors *) val error_invalid_pattern_notation : ?loc:Loc.t -> unit -> 'a -(** Placeholder for global option, should be moved to a parameter *) -val asymmetric_patterns : bool ref - (** Local universe and constraint declarations. *) val interp_univ_decl : Environ.env -> universe_decl_expr -> Evd.evar_map * UState.universe_decl diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 0f5fa14c23..25f2526f74 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -193,17 +193,12 @@ let without_specific_symbols l = (* Control printing of records *) (* Set Record Printing flag *) -let record_print = ref true - -let () = - let open Goptions in - declare_bool_option - { optdepr = false; - optname = "record printing"; - optkey = ["Printing";"Records"]; - optread = (fun () -> !record_print); - optwrite = (fun b -> record_print := b) } - +let get_record_print = + Goptions.declare_bool_option_and_ref + ~depr:false + ~name:"record printing" + ~key:["Printing";"Records"] + ~value:true let is_record indsp = try @@ -431,7 +426,7 @@ let rec extern_cases_pattern_in_scope (custom,scopes as allscopes) vars pat = with Not_found | No_match | Exit -> let c = extern_reference Id.Set.empty (ConstructRef cstrsp) in - if !asymmetric_patterns then + if Constrintern.get_asymmetric_patterns () then if pattern_printable_in_both_syntax cstrsp then CPatCstr (c, None, args) else CPatCstr (c, Some (add_patt_for_params (fst cstrsp) args), []) @@ -469,7 +464,7 @@ and apply_notation_to_pattern ?loc gr ((subst,substlist),(nb_to_drop,more_args)) List.map (extern_cases_pattern_in_scope subscope vars) c) substlist in let l2 = List.map (extern_cases_pattern_in_scope allscopes vars) more_args in - let l2' = if !asymmetric_patterns || not (List.is_empty ll) then l2 + let l2' = if Constrintern.get_asymmetric_patterns () || not (List.is_empty ll) then l2 else match drop_implicits_in_patt gr nb_to_drop l2 with |Some true_args -> true_args @@ -489,7 +484,7 @@ and apply_notation_to_pattern ?loc gr ((subst,substlist),(nb_to_drop,more_args)) extern_cases_pattern_in_scope (subentry,(scopt,scl@scopes)) vars c) subst in let l2 = List.map (extern_cases_pattern_in_scope allscopes vars) more_args in - let l2' = if !asymmetric_patterns then l2 + let l2' = if Constrintern.get_asymmetric_patterns () then l2 else match drop_implicits_in_patt gr (nb_to_drop + List.length l1) l2 with |Some true_args -> true_args @@ -824,7 +819,7 @@ let rec extern inctx scopes vars r = () else if PrintingConstructor.active (fst cstrsp) then raise Exit - else if not !record_print then + else if not (get_record_print ()) then raise Exit; let projs = struc.Recordops.s_PROJ in let locals = struc.Recordops.s_PROJKIND in diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 02db8f6aab..6313f2d7ba 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1488,6 +1488,12 @@ let is_non_zero_pat c = match c with | { CAst.v = CPatPrim (Numeral (p, true)) } -> not (is_zero p) | _ -> false +let get_asymmetric_patterns = Goptions.declare_bool_option_and_ref + ~depr:false + ~name:"no parameters in constructors" + ~key:["Asymmetric";"Patterns"] + ~value:false + let drop_notations_pattern looked_for genv = (* At toplevel, Constructors and Inductives are accepted, in recursive calls only constructor are allowed *) @@ -1562,7 +1568,7 @@ let drop_notations_pattern looked_for genv = | None -> DAst.make ?loc @@ RCPatAtom None | Some (n, head, pl) -> let pl = - if !asymmetric_patterns then pl else + if get_asymmetric_patterns () then pl else let pars = List.make n (CAst.make ?loc @@ CPatAtom None) in List.rev_append pars pl in match drop_syndef top scopes head pl with @@ -1684,7 +1690,7 @@ let rec intern_pat genv ntnvars aliases pat = let aliases' = merge_aliases aliases id in intern_pat genv ntnvars aliases' p | RCPatCstr (head, expl_pl, pl) -> - if !asymmetric_patterns then + if get_asymmetric_patterns () then let len = if List.is_empty expl_pl then Some (List.length pl) else None in let c,idslpl1 = find_constructor loc len head in let with_letin = diff --git a/interp/constrintern.mli b/interp/constrintern.mli index 147a903fe2..035e4bc644 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -197,3 +197,6 @@ val parsing_explicit : bool ref (** Globalization leak for Grammar *) val for_grammar : ('a -> 'b) -> 'a -> 'b + +(** Placeholder for global option, should be moved to a parameter *) +val get_asymmetric_patterns : unit -> bool diff --git a/lib/flags.ml b/lib/flags.ml index 3aef5a7b2c..ae4d337ded 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -123,8 +123,5 @@ let get_inline_level () = !inline_level (* Native code compilation for conversion and normalization *) let output_native_objects = ref false -(* Print the mod uid associated to a vo file by the native compiler *) -let print_mod_uid = ref false - let profile_ltac = ref false let profile_ltac_cutoff = ref 2.0 diff --git a/lib/flags.mli b/lib/flags.mli index e282d4ca8c..d883cf1e30 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -119,8 +119,6 @@ val default_inline_level : int (** When producing vo objects, also compile the native-code version *) val output_native_objects : bool ref -(** Print the mod uid associated to a vo file by the native compiler *) -val print_mod_uid : bool ref - +(** Global profile_ltac flag *) val profile_ltac : bool ref val profile_ltac_cutoff : float ref diff --git a/library/goptions.ml b/library/goptions.ml index bb9b4e29fc..98efb512ab 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -299,6 +299,18 @@ let declare_stringopt_option = (function StringOptValue v -> v | _ -> anomaly (Pp.str "async_option.")) (fun _ _ -> anomaly (Pp.str "async_option.")) +let declare_bool_option_and_ref ~depr ~name ~key ~(value:bool) = + let r_opt = ref value in + let optwrite v = r_opt := v in + let optread () = !r_opt in + let _ = declare_bool_option { + optdepr = depr; + optname = name; + optkey = key; + optread; optwrite + } in + optread + (* 3- User accessible commands *) (* Setting values of options *) @@ -422,6 +434,3 @@ let print_tables () = (fun (nickkey,_) p -> p ++ str " " ++ str nickkey ++ fnl ()) !ref_table (mt ()) ++ fnl () - - - diff --git a/library/goptions.mli b/library/goptions.mli index 900217e06b..b91553bf3c 100644 --- a/library/goptions.mli +++ b/library/goptions.mli @@ -131,6 +131,9 @@ val declare_string_option: ?preprocess:(string -> string) -> val declare_stringopt_option: ?preprocess:(string option -> string option) -> string option option_sig -> unit +(** Helper to declare a reference controlled by an option. Read-only + as to avoid races. *) +val declare_bool_option_and_ref : depr:bool -> name:string -> key:option_name -> value:bool -> (unit -> bool) (** {6 Special functions supposed to be used only in vernacentries.ml } *) diff --git a/parsing/extend.ml b/parsing/extend.ml index 5caeab535a..050ed49622 100644 --- a/parsing/extend.ml +++ b/parsing/extend.ml @@ -14,17 +14,8 @@ type 'a entry = 'a Gramlib.Grammar.GMake(CLexer).Entry.e type side = Left | Right -type gram_assoc = NonA | RightA | LeftA - -type gram_position = - | First - | Last - | Before of string - | After of string - | Level of string - type production_position = - | BorderProd of side * gram_assoc option + | BorderProd of side * Gramlib.Gramext.g_assoc option | InternalProd type production_level = @@ -116,11 +107,11 @@ type 'a production_rule = type 'a single_extend_statement = string option * (** Level *) - gram_assoc option * + Gramlib.Gramext.g_assoc option * (** Associativity *) 'a production_rule list (** Symbol list with the interpretation function *) type 'a extend_statement = - gram_position option * + Gramlib.Gramext.position option * 'a single_extend_statement list diff --git a/parsing/notation_gram.ml b/parsing/notation_gram.ml index d8c08803b6..fc5feba58b 100644 --- a/parsing/notation_gram.ml +++ b/parsing/notation_gram.ml @@ -32,7 +32,7 @@ type grammar_constr_prod_item = type one_notation_grammar = { notgram_level : level; - notgram_assoc : Extend.gram_assoc option; + notgram_assoc : Gramlib.Gramext.g_assoc option; notgram_notation : Constrexpr.notation; notgram_prods : grammar_constr_prod_item list list; } diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index 170df6ad09..816a02a6aa 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -14,8 +14,6 @@ open Extend open Genarg open Gramlib -let uncurry f (x,y) = f x y - (** Location Utils *) let ploc_file_of_coq_file = function | Loc.ToplevelInput -> "" @@ -82,7 +80,6 @@ module type S = end *) - type 'a entry = 'a Entry.e type coq_parsable val coq_parsable : ?file:Loc.source -> char Stream.t -> coq_parsable @@ -91,12 +88,10 @@ module type S = val comment_state : coq_parsable -> ((int * int) * string) list -end with type 'a Entry.e = 'a Grammar.GMake(CLexer).Entry.e = struct +end with type 'a Entry.e = 'a Extend.entry = struct include Grammar.GMake(CLexer) - type 'a entry = 'a Entry.e - type coq_parsable = parsable * CLexer.lexer_state ref let coq_parsable ?(file=Loc.ToplevelInput) c = @@ -146,20 +141,6 @@ struct end -let warning_verbose = Gramext.warning_verbose - -let of_coq_assoc = function -| Extend.RightA -> Gramext.RightA -| Extend.LeftA -> Gramext.LeftA -| Extend.NonA -> Gramext.NonA - -let of_coq_position = function -| Extend.First -> Gramext.First -| Extend.Last -> Gramext.Last -| Extend.Before s -> Gramext.Before s -| Extend.After s -> Gramext.After s -| Extend.Level s -> Gramext.Level s - module Symbols : sig val stoken : Tok.t -> ('s, string) G.ty_symbol val slist0sep : ('s, 'a) G.ty_symbol -> ('s, 'b) G.ty_symbol -> ('s, 'a list) G.ty_symbol @@ -184,12 +165,6 @@ end = struct let slist1sep x y = G.s_list1sep x y false end -let camlp5_verbosity silent f x = - let a = !warning_verbose in - warning_verbose := silent; - f x; - warning_verbose := a - (** Grammar extensions *) (** NB: [extend_statement = @@ -218,7 +193,9 @@ let rec symbol_of_prod_entry_key : type s a. (s, a) symbol -> (s, a) G.ty_symbol | Anext -> G.s_next | Aentry e -> G.s_nterm e | Aentryl (e, n) -> G.s_nterml e n -| Arules rs -> G.s_rules (List.map symbol_of_rules rs) +| Arules rs -> + let warning msg = Feedback.msg_warning Pp.(str msg) in + G.s_rules ~warning:(Some warning) (List.map symbol_of_rules rs) and symbol_of_rule : type s a r. (s, a, Loc.t -> r) Extend.rule -> (s, a, Ploc.t -> r) casted_rule = function | Stop -> Casted (G.r_stop, fun act loc -> act (!@loc)) @@ -240,10 +217,10 @@ let of_coq_production_rule : type a. a Extend.production_rule -> a any_productio AnyProduction (symb, cast act) let of_coq_single_extend_statement (lvl, assoc, rule) = - (lvl, Option.map of_coq_assoc assoc, List.map of_coq_production_rule rule) + (lvl, assoc, List.map of_coq_production_rule rule) let of_coq_extend_statement (pos, st) = - (Option.map of_coq_position pos, List.map of_coq_single_extend_statement st) + (pos, List.map of_coq_single_extend_statement st) let fix_extend_statement (pos, st) = let fix_single_extend_statement (lvl, assoc, rules) = @@ -253,19 +230,19 @@ let fix_extend_statement (pos, st) = (pos, List.map fix_single_extend_statement st) (** Type of reinitialization data *) -type gram_reinit = gram_assoc * gram_position +type gram_reinit = Gramlib.Gramext.g_assoc * Gramlib.Gramext.position type extend_rule = -| ExtendRule : 'a G.entry * gram_reinit option * 'a extend_statement -> extend_rule +| ExtendRule : 'a G.Entry.e * gram_reinit option * 'a extend_statement -> extend_rule module EntryCommand = Dyn.Make () -module EntryData = struct type _ t = Ex : 'b G.entry String.Map.t -> ('a * 'b) t end +module EntryData = struct type _ t = Ex : 'b G.Entry.e String.Map.t -> ('a * 'b) t end module EntryDataMap = EntryCommand.Map(EntryData) type ext_kind = | ByGrammar of extend_rule | ByEXTEND of (unit -> unit) * (unit -> unit) - | ByEntry : ('a * 'b) EntryCommand.tag * string * 'b G.entry -> ext_kind + | ByEntry : ('a * 'b) EntryCommand.tag * string * 'b G.Entry.e -> ext_kind (** The list of extensions *) @@ -282,13 +259,12 @@ let grammar_delete e reinit (pos,rls) = (List.rev rls); match reinit with | Some (a,ext) -> - let a = of_coq_assoc a in - let ext = of_coq_position ext in let lev = match pos with | Some (Gramext.Level n) -> n | _ -> assert false in - (G.safe_extend e) (Some ext) [Some lev,Some a,[]] + let warning msg = Feedback.msg_warning Pp.(str msg) in + (G.safe_extend ~warning:(Some warning) e) (Some ext) [Some lev,Some a,[]] | None -> () (** Extension *) @@ -296,15 +272,15 @@ let grammar_delete e reinit (pos,rls) = let grammar_extend e reinit ext = let ext = of_coq_extend_statement ext in let undo () = grammar_delete e reinit ext in - let ext = fix_extend_statement ext in - let redo () = camlp5_verbosity false (uncurry (G.safe_extend e)) ext in + let pos, ext = fix_extend_statement ext in + let redo () = G.safe_extend ~warning:None e pos ext in camlp5_state := ByEXTEND (undo, redo) :: !camlp5_state; redo () let grammar_extend_sync e reinit ext = camlp5_state := ByGrammar (ExtendRule (e, reinit, ext)) :: !camlp5_state; - let ext = fix_extend_statement (of_coq_extend_statement ext) in - camlp5_verbosity false (uncurry (G.safe_extend e)) ext + let pos, ext = fix_extend_statement (of_coq_extend_statement ext) in + G.safe_extend ~warning:None e pos ext (** The apparent parser of Coq; encapsulate G to keep track of the extensions. *) @@ -352,14 +328,16 @@ let eoi_entry en = let e = Entry.create ((Gram.Entry.name en) ^ "_eoi") in let symbs = G.r_next (G.r_next G.r_stop (G.s_nterm en)) (Symbols.stoken Tok.EOI) in let act = fun _ x loc -> x in - Gram.safe_extend e None (make_rule [G.production (symbs, act)]); + let warning msg = Feedback.msg_warning Pp.(str msg) in + Gram.safe_extend ~warning:(Some warning) e None (make_rule [G.production (symbs, act)]); e let map_entry f en = let e = Entry.create ((Gram.Entry.name en) ^ "_map") in let symbs = G.r_next G.r_stop (G.s_nterm en) in let act = fun x loc -> f x in - Gram.safe_extend e None (make_rule [G.production (symbs, act)]); + let warning msg = Feedback.msg_warning Pp.(str msg) in + Gram.safe_extend ~warning:(Some warning) e None (make_rule [G.production (symbs, act)]); e (* Parse a string, does NOT check if the entire string was read @@ -489,7 +467,8 @@ let epsilon_value f e = let r = G.production (G.r_next G.r_stop (symbol_of_prod_entry_key e), (fun x _ -> f x)) in let ext = [None, None, [r]] in let entry = Gram.entry_create "epsilon" in - let () = G.safe_extend entry None ext in + let warning msg = Feedback.msg_warning Pp.(str msg) in + let () = G.safe_extend ~warning:(Some warning) entry None ext in try Some (parse_string entry "") with _ -> None (** Synchronized grammar extensions *) @@ -542,7 +521,7 @@ let extend_grammar_command tag g = let nb = List.length rules in grammar_stack := (GramExt (nb, GrammarCommand.Dyn (tag, g)), st) :: !grammar_stack -let extend_entry_command (type a) (type b) (tag : (a, b) entry_command) (g : a) : b Gram.entry list = +let extend_entry_command (type a) (type b) (tag : (a, b) entry_command) (g : a) : b Gram.Entry.e list = let EntryInterp.Ex modify = EntryInterpMap.find tag !entry_interp in let grammar_state = match !grammar_stack with | [] -> GramState.empty @@ -574,7 +553,7 @@ let extend_dyn_grammar (e, _) = match e with (** Registering extra grammar *) -type any_entry = AnyEntry : 'a Gram.entry -> any_entry +type any_entry = AnyEntry : 'a Gram.Entry.e -> any_entry let grammar_names : any_entry list String.Map.t ref = ref String.Map.empty diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index e64c614149..69ba57d516 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -26,7 +26,7 @@ sig end module Entry : sig - type 'a t = 'a Grammar.GMake(CLexer).Entry.e + type 'a t = 'a Extend.entry val create : string -> 'a t val parse : 'a t -> Parsable.t -> 'a val print : Format.formatter -> 'a t -> unit @@ -110,10 +110,6 @@ end *) -(** Temporarily activate camlp5 verbosity *) - -val camlp5_verbosity : bool -> ('a -> unit) -> 'a -> unit - (** Parse a string *) val parse_string : 'a Entry.t -> string -> 'a @@ -202,7 +198,7 @@ val epsilon_value : ('a -> 'self) -> ('self, 'a) Extend.symbol -> 'self option (** {5 Extending the parser without synchronization} *) -type gram_reinit = gram_assoc * gram_position +type gram_reinit = Gramlib.Gramext.g_assoc * Gramlib.Gramext.position (** Type of reinitialization data *) val grammar_extend : 'a Entry.t -> gram_reinit option -> diff --git a/plugins/ltac/extraargs.mli b/plugins/ltac/extraargs.mli index fa70235975..0509d6ae71 100644 --- a/plugins/ltac/extraargs.mli +++ b/plugins/ltac/extraargs.mli @@ -8,6 +8,7 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +open Genintern open Tacexpr open Names open Constrexpr @@ -28,22 +29,22 @@ val wit_natural : int Genarg.uniform_genarg_type val wit_glob : (constr_expr, - Tacexpr.glob_constr_and_expr, + glob_constr_and_expr, Tacinterp.interp_sign * glob_constr) Genarg.genarg_type val wit_lglob : (constr_expr, - Tacexpr.glob_constr_and_expr, + glob_constr_and_expr, Tacinterp.interp_sign * glob_constr) Genarg.genarg_type val wit_lconstr : (constr_expr, - Tacexpr.glob_constr_and_expr, + glob_constr_and_expr, EConstr.t) Genarg.genarg_type val wit_casted_constr : (constr_expr, - Tacexpr.glob_constr_and_expr, + glob_constr_and_expr, EConstr.t) Genarg.genarg_type val glob : constr_expr Pcoq.Entry.t diff --git a/plugins/ltac/extratactics.mli b/plugins/ltac/extratactics.mli index 7fb9a19a0c..4576562634 100644 --- a/plugins/ltac/extratactics.mli +++ b/plugins/ltac/extratactics.mli @@ -14,4 +14,4 @@ val injHyp : Names.Id.t -> unit Proofview.tactic (* val refine_tac : Evd.open_constr -> unit Proofview.tactic *) -val onSomeWithHoles : ('a option -> unit Proofview.tactic) -> 'a Tacexpr.delayed_open option -> unit Proofview.tactic +val onSomeWithHoles : ('a option -> unit Proofview.tactic) -> 'a Tactypes.delayed_open option -> unit Proofview.tactic diff --git a/plugins/ltac/g_rewrite.mlg b/plugins/ltac/g_rewrite.mlg index f7375a0f01..31fb1c9abf 100644 --- a/plugins/ltac/g_rewrite.mlg +++ b/plugins/ltac/g_rewrite.mlg @@ -16,6 +16,7 @@ open Names open Locus open Constrexpr open Glob_term +open Genintern open Geninterp open Extraargs open Tacmach @@ -37,8 +38,8 @@ DECLARE PLUGIN "ltac_plugin" { type constr_expr_with_bindings = constr_expr with_bindings -type glob_constr_with_bindings = Tacexpr.glob_constr_and_expr with_bindings -type glob_constr_with_bindings_sign = interp_sign * Tacexpr.glob_constr_and_expr with_bindings +type glob_constr_with_bindings = glob_constr_and_expr with_bindings +type glob_constr_with_bindings_sign = interp_sign * glob_constr_and_expr with_bindings let pr_glob_constr_with_bindings_sign _ _ _ (ge : glob_constr_with_bindings_sign) = let _, env = Pfedit.get_current_context () in @@ -70,7 +71,7 @@ END { type raw_strategy = (constr_expr, Tacexpr.raw_red_expr) strategy_ast -type glob_strategy = (Tacexpr.glob_constr_and_expr, Tacexpr.raw_red_expr) strategy_ast +type glob_strategy = (glob_constr_and_expr, Tacexpr.raw_red_expr) strategy_ast let interp_strategy ist gl s = let sigma = project gl in diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index 50cfb6d004..55e58187b0 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -26,6 +26,7 @@ open Pputils open Ppconstr open Printer +open Genintern open Tacexpr open Tacarg open Tactics diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli index 6c09e447a5..0ab9e501bc 100644 --- a/plugins/ltac/pptactic.mli +++ b/plugins/ltac/pptactic.mli @@ -17,6 +17,7 @@ open Names open Environ open Constrexpr open Notation_gram +open Genintern open Tacexpr open Tactypes diff --git a/plugins/ltac/rewrite.mli b/plugins/ltac/rewrite.mli index 4f46e78c71..2457b265f0 100644 --- a/plugins/ltac/rewrite.mli +++ b/plugins/ltac/rewrite.mli @@ -13,6 +13,7 @@ open Environ open EConstr open Constrexpr open Evd +open Genintern open Tactypes open Tacexpr open Tacinterp diff --git a/plugins/ltac/tacarg.mli b/plugins/ltac/tacarg.mli index bdb0be03cf..0c7096a4de 100644 --- a/plugins/ltac/tacarg.mli +++ b/plugins/ltac/tacarg.mli @@ -11,6 +11,7 @@ open Genarg open EConstr open Constrexpr +open Genintern open Tactypes open Tacexpr diff --git a/plugins/ltac/taccoerce.mli b/plugins/ltac/taccoerce.mli index d2ae92f6ce..b04c3b9f4e 100644 --- a/plugins/ltac/taccoerce.mli +++ b/plugins/ltac/taccoerce.mli @@ -53,7 +53,7 @@ val coerce_var_to_ident : bool -> Environ.env -> Evd.evar_map -> Value.t -> Id.t val coerce_to_ident_not_fresh : Evd.evar_map -> Value.t -> Id.t -val coerce_to_intro_pattern : Evd.evar_map -> Value.t -> Tacexpr.delayed_open_constr intro_pattern_expr +val coerce_to_intro_pattern : Evd.evar_map -> Value.t -> delayed_open_constr intro_pattern_expr val coerce_to_intro_pattern_naming : Evd.evar_map -> Value.t -> Namegen.intro_pattern_naming_expr diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml index ac2d88dec2..2aee809eb6 100644 --- a/plugins/ltac/tacentries.ml +++ b/plugins/ltac/tacentries.ml @@ -119,7 +119,7 @@ let get_tactic_entry n = else if Int.equal n 5 then Pltac.binder_tactic, None else if 1<=n && n<5 then - Pltac.tactic_expr, Some (Extend.Level (string_of_int n)) + Pltac.tactic_expr, Some (Gramlib.Gramext.Level (string_of_int n)) else user_err Pp.(str ("Invalid Tactic Notation level: "^(string_of_int n)^".")) diff --git a/plugins/ltac/tacexpr.ml b/plugins/ltac/tacexpr.ml index 9435d0b911..2bd21f9d7a 100644 --- a/plugins/ltac/tacexpr.ml +++ b/plugins/ltac/tacexpr.ml @@ -93,19 +93,8 @@ type ml_tactic_entry = { (** Composite types *) -type glob_constr_and_expr = Genintern.glob_constr_and_expr - type open_constr_expr = unit * constr_expr -type open_glob_constr = unit * glob_constr_and_expr - -type binding_bound_vars = Constr_matching.binding_bound_vars -type glob_constr_pattern_and_expr = binding_bound_vars * glob_constr_and_expr * constr_pattern - -type 'a delayed_open = Environ.env -> Evd.evar_map -> Evd.evar_map * 'a - -type delayed_open_constr_with_bindings = EConstr.constr with_bindings delayed_open - -type delayed_open_constr = EConstr.constr delayed_open +type open_glob_constr = unit * Genintern.glob_constr_and_expr type intro_pattern = delayed_open_constr intro_pattern_expr CAst.t type intro_patterns = delayed_open_constr intro_pattern_expr CAst.t list @@ -279,8 +268,8 @@ constraint 'a = < (** Globalized tactics *) -type g_trm = glob_constr_and_expr -type g_pat = glob_constr_pattern_and_expr +type g_trm = Genintern.glob_constr_and_expr +type g_pat = Genintern.glob_constr_pattern_and_expr type g_cst = evaluable_global_reference Stdarg.and_short_name or_var type g_ref = ltac_constant located or_var type g_nam = lident diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli index 1527724420..0c27f3bfe2 100644 --- a/plugins/ltac/tacexpr.mli +++ b/plugins/ltac/tacexpr.mli @@ -92,20 +92,8 @@ type ml_tactic_entry = { } (** Composite types *) - -type glob_constr_and_expr = Genintern.glob_constr_and_expr - type open_constr_expr = unit * constr_expr -type open_glob_constr = unit * glob_constr_and_expr - -type binding_bound_vars = Constr_matching.binding_bound_vars -type glob_constr_pattern_and_expr = binding_bound_vars * glob_constr_and_expr * constr_pattern - -type 'a delayed_open = Environ.env -> Evd.evar_map -> Evd.evar_map * 'a - -type delayed_open_constr_with_bindings = EConstr.constr with_bindings delayed_open - -type delayed_open_constr = EConstr.constr delayed_open +type open_glob_constr = unit * Genintern.glob_constr_and_expr type intro_pattern = delayed_open_constr intro_pattern_expr CAst.t type intro_patterns = delayed_open_constr intro_pattern_expr CAst.t list @@ -279,8 +267,8 @@ constraint 'a = < (** Globalized tactics *) -type g_trm = glob_constr_and_expr -type g_pat = glob_constr_pattern_and_expr +type g_trm = Genintern.glob_constr_and_expr +type g_pat = Genintern.glob_constr_pattern_and_expr type g_cst = evaluable_global_reference Stdarg.and_short_name or_var type g_ref = ltac_constant located or_var type g_nam = lident diff --git a/plugins/ltac/tacintern.mli b/plugins/ltac/tacintern.mli index 178f6af71d..978ad4dd24 100644 --- a/plugins/ltac/tacintern.mli +++ b/plugins/ltac/tacintern.mli @@ -12,6 +12,7 @@ open Names open Tacexpr open Genarg open Constrexpr +open Genintern open Tactypes (** Globalization of tactic expressions : diff --git a/plugins/ltac/tacinterp.mli b/plugins/ltac/tacinterp.mli index f9883e4441..d9c80bb835 100644 --- a/plugins/ltac/tacinterp.mli +++ b/plugins/ltac/tacinterp.mli @@ -43,6 +43,8 @@ type interp_sign = Geninterp.interp_sign = { lfun : value Id.Map.t; extra : TacStore.t } +open Genintern + val f_avoid_ids : Id.Set.t TacStore.field val f_debug : debug_info TacStore.field diff --git a/plugins/ltac/tacsubst.mli b/plugins/ltac/tacsubst.mli index d406686c56..4487604dca 100644 --- a/plugins/ltac/tacsubst.mli +++ b/plugins/ltac/tacsubst.mli @@ -11,6 +11,7 @@ open Tacexpr open Mod_subst open Genarg +open Genintern open Tactypes (** Substitution of tactics at module closing time *) diff --git a/plugins/ltac/tactic_debug.mli b/plugins/ltac/tactic_debug.mli index 175341df09..91e8510b92 100644 --- a/plugins/ltac/tactic_debug.mli +++ b/plugins/ltac/tactic_debug.mli @@ -40,7 +40,7 @@ val db_constr : debug_info -> env -> evar_map -> constr -> unit Proofview.NonLog (** Prints the pattern rule *) val db_pattern_rule : - debug_info -> int -> (Tacexpr.glob_constr_and_expr * constr_pattern,glob_tactic_expr) match_rule -> unit Proofview.NonLogical.t + debug_info -> int -> (Genintern.glob_constr_and_expr * constr_pattern,glob_tactic_expr) match_rule -> unit Proofview.NonLogical.t (** Prints a matched hypothesis *) val db_matched_hyp : diff --git a/plugins/ltac/tactic_matching.mli b/plugins/ltac/tactic_matching.mli index 0722c68783..457c4e0b9a 100644 --- a/plugins/ltac/tactic_matching.mli +++ b/plugins/ltac/tactic_matching.mli @@ -35,7 +35,7 @@ val match_term : Environ.env -> Evd.evar_map -> EConstr.constr -> - (Tacexpr.binding_bound_vars * Pattern.constr_pattern, Tacexpr.glob_tactic_expr) Tacexpr.match_rule list -> + (Constr_matching.binding_bound_vars * Pattern.constr_pattern, Tacexpr.glob_tactic_expr) Tacexpr.match_rule list -> Tacexpr.glob_tactic_expr t Proofview.tactic (** [match_goal env sigma hyps concl rules] matches the goal @@ -48,5 +48,5 @@ val match_goal: Evd.evar_map -> EConstr.named_context -> EConstr.constr -> - (Tacexpr.binding_bound_vars * Pattern.constr_pattern, Tacexpr.glob_tactic_expr) Tacexpr.match_rule list -> + (Constr_matching.binding_bound_vars * Pattern.constr_pattern, Tacexpr.glob_tactic_expr) Tacexpr.match_rule list -> Tacexpr.glob_tactic_expr t Proofview.tactic diff --git a/plugins/ssr/ssrast.mli b/plugins/ssr/ssrast.mli index a786b9953d..bb8a0faf2e 100644 --- a/plugins/ssr/ssrast.mli +++ b/plugins/ssr/ssrast.mli @@ -47,7 +47,7 @@ type ssrdocc = ssrclear option * ssrocc (* OLD ssr terms *) type ssrtermkind = char (* FIXME, make algebraic *) -type ssrterm = ssrtermkind * Tacexpr.glob_constr_and_expr +type ssrterm = ssrtermkind * Genintern.glob_constr_and_expr (* NEW ssr term *) diff --git a/plugins/ssr/ssrcommon.mli b/plugins/ssr/ssrcommon.mli index e25c93bf0a..824827e90c 100644 --- a/plugins/ssr/ssrcommon.mli +++ b/plugins/ssr/ssrcommon.mli @@ -146,7 +146,7 @@ val interp_refine : val interp_open_constr : Tacinterp.interp_sign -> Goal.goal Evd.sigma -> - Tacexpr.glob_constr_and_expr -> evar_map * (evar_map * EConstr.t) + Genintern.glob_constr_and_expr -> evar_map * (evar_map * EConstr.t) val pf_e_type_of : Goal.goal Evd.sigma -> diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg index b48030b963..c9221ef758 100644 --- a/plugins/ssr/ssrparser.mlg +++ b/plugins/ssr/ssrparser.mlg @@ -576,6 +576,8 @@ END { +type ssrfwdview = ast_closure_term list + let pr_ssrfwdview _ _ _ = pr_view2 } @@ -637,6 +639,7 @@ let rec map_ipat map_id map_ssrhyp map_ast_closure_term = function | IPatView (clr,v) -> IPatView (clr,List.map map_ast_closure_term v) | IPatTac _ -> assert false (*internal usage only *) +type ssripatrep = ssripat let wit_ssripatrep = add_genarg "ssripatrep" pr_ipat let pr_ssripat _ _ _ = pr_ipat @@ -1933,6 +1936,7 @@ END (* argument *) { +type ssreqid = ssripatrep option let pr_eqid = function Some pat -> str " " ++ pr_ipat pat | None -> mt () let pr_ssreqid _ _ _ = pr_eqid @@ -1987,10 +1991,12 @@ END (* the entry point parses only non-empty arguments to avoid conflicts *) (* with the basic Coq tactics. *) -(* type ssrarg = ssrbwdview * (ssreqid * (ssrdgens * ssripats)) *) - { +type ssrarg = ssrfwdview * (ssreqid * (cpattern ssragens * ssripats)) + +(* type ssrarg = ssrbwdview * (ssreqid * (ssrdgens * ssripats)) *) + let pr_ssrarg _ _ _ (view, (eqid, (dgens, ipats))) = let pri = pr_intros (gens_sep dgens) in pr_view2 view ++ pr_eqid eqid ++ pr_dgens pr_gen dgens ++ pri ipats diff --git a/plugins/ssr/ssrparser.mli b/plugins/ssr/ssrparser.mli index 862a93765d..a2cbd3c9c8 100644 --- a/plugins/ssr/ssrparser.mli +++ b/plugins/ssr/ssrparser.mli @@ -28,10 +28,22 @@ open Ssrmatching open Ssrast open Ssrequality +type ssrfwdview = ast_closure_term list +type ssreqid = ssripat option +type ssrarg = ssrfwdview * (ssreqid * (cpattern ssragens * ssripats)) + +val wit_ssripatrep : ssripat Genarg.uniform_genarg_type +val wit_ssrarg : ssrarg Genarg.uniform_genarg_type val wit_ssrrwargs : ssrrwarg list Genarg.uniform_genarg_type val wit_ssrclauses : clauses Genarg.uniform_genarg_type val wit_ssrcasearg : (cpattern ssragens) ssrmovearg Genarg.uniform_genarg_type val wit_ssrmovearg : (cpattern ssragens) ssrmovearg Genarg.uniform_genarg_type val wit_ssrapplyarg : ssrapplyarg Genarg.uniform_genarg_type val wit_ssrhavefwdwbinders : - (Tacexpr.raw_tactic_expr fwdbinders, Tacexpr.glob_tactic_expr fwdbinders, Tacinterp.Value.t fwdbinders) Genarg.genarg_type + (Tacexpr.raw_tactic_expr fwdbinders, + Tacexpr.glob_tactic_expr fwdbinders, + Tacinterp.Value.t fwdbinders) Genarg.genarg_type +val wit_ssrhintarg : + (Tacexpr.raw_tactic_expr ssrhint, + Tacexpr.glob_tactic_expr ssrhint, + Tacinterp.Value.t ssrhint) Genarg.genarg_type diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml index 8cb0a8b463..6497b6ff98 100644 --- a/plugins/ssrmatching/ssrmatching.ml +++ b/plugins/ssrmatching/ssrmatching.ml @@ -896,7 +896,7 @@ let interp_rpattern s = function let interp_rpattern0 ist gl t = Tacmach.project gl, interp_rpattern ist t -type cpattern = char * glob_constr_and_expr * Geninterp.interp_sign option +type cpattern = char * Genintern.glob_constr_and_expr * Geninterp.interp_sign option let tag_of_cpattern = pi1 let loc_of_cpattern = loc_ofCG let cpattern_of_term (c, t) ist = c, t, Some ist diff --git a/plugins/ssrmatching/ssrmatching.mli b/plugins/ssrmatching/ssrmatching.mli index 93a8c48435..8672c55767 100644 --- a/plugins/ssrmatching/ssrmatching.mli +++ b/plugins/ssrmatching/ssrmatching.mli @@ -5,9 +5,7 @@ open Goal open Environ open Evd open Constr - -open Ltac_plugin -open Tacexpr +open Genintern (** ******** Small Scale Reflection pattern matching facilities ************* *) diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml index 7104b8586e..f8289f558c 100644 --- a/pretyping/cbv.ml +++ b/pretyping/cbv.ml @@ -183,14 +183,11 @@ let cofixp_reducible flgs _ stk = else false -let debug_cbv = ref false -let () = Goptions.(declare_bool_option { - optdepr = false; - optname = "cbv visited constants display"; - optkey = ["Debug";"Cbv"]; - optread = (fun () -> !debug_cbv); - optwrite = (fun a -> debug_cbv:=a); -}) +let get_debug_cbv = Goptions.declare_bool_option_and_ref + ~depr:false + ~value:false + ~name:"cbv visited constants display" + ~key:["Debug";"Cbv"] let debug_pr_key = function | ConstKey (sp,_) -> Names.Constant.print sp @@ -325,14 +322,14 @@ and norm_head_ref k info env stack normt = if red_set_ref info.reds normt then match cbv_value_cache info normt with | Some body -> - if !debug_cbv then Feedback.msg_debug Pp.(str "Unfolding " ++ debug_pr_key normt); + if get_debug_cbv () then Feedback.msg_debug Pp.(str "Unfolding " ++ debug_pr_key normt); strip_appl (shift_value k body) stack | None -> - if !debug_cbv then Feedback.msg_debug Pp.(str "Not unfolding " ++ debug_pr_key normt); + if get_debug_cbv () then Feedback.msg_debug Pp.(str "Not unfolding " ++ debug_pr_key normt); (VAL(0,make_constr_ref k normt),stack) else begin - if !debug_cbv then Feedback.msg_debug Pp.(str "Not unfolding " ++ debug_pr_key normt); + if get_debug_cbv () then Feedback.msg_debug Pp.(str "Not unfolding " ++ debug_pr_key normt); (VAL(0,make_constr_ref k normt),stack) end diff --git a/pretyping/classops.ml b/pretyping/classops.ml index 1edcc499f0..f18040accb 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -398,16 +398,12 @@ let class_params = function let add_class cl = add_new_class cl { cl_param = class_params cl } -let automatically_import_coercions = ref false - -open Goptions -let () = - declare_bool_option - { optdepr = true; (* remove in 8.8 *) - optname = "automatic import of coercions"; - optkey = ["Automatic";"Coercions";"Import"]; - optread = (fun () -> !automatically_import_coercions); - optwrite = (:=) automatically_import_coercions } +let get_automatically_import_coercions = + Goptions.declare_bool_option_and_ref + ~depr:true (* Remove in 8.8 *) + ~name:"automatic import of coercions" + ~key:["Automatic";"Coercions";"Import"] + ~value:false let cache_coercion (_, c) = let () = add_class c.coercion_source in @@ -425,7 +421,7 @@ let cache_coercion (_, c) = add_coercion_in_graph (xf,is,it) let load_coercion _ o = - if !automatically_import_coercions then + if get_automatically_import_coercions () then cache_coercion o let set_coercion_in_scope (_, c) = @@ -435,7 +431,7 @@ let set_coercion_in_scope (_, c) = let open_coercion i o = if Int.equal i 1 then begin set_coercion_in_scope o; - if not !automatically_import_coercions then + if not (get_automatically_import_coercions ()) then cache_coercion o end diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index 30eb70d0e7..4d1d405bd7 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -33,16 +33,12 @@ open Evd open Termops open Globnames -let use_typeclasses_for_conversion = ref true - -let () = - Goptions.(declare_bool_option - { optdepr = false; - optname = "use typeclass resolution during conversion"; - optkey = ["Typeclass"; "Resolution"; "For"; "Conversion"]; - optread = (fun () -> !use_typeclasses_for_conversion); - optwrite = (fun b -> use_typeclasses_for_conversion := b) } - ) +let get_use_typeclasses_for_conversion = + Goptions.declare_bool_option_and_ref + ~depr:false + ~name:"use typeclass resolution during conversion" + ~key:["Typeclass"; "Resolution"; "For"; "Conversion"] + ~value:true (* Typing operations dealing with coercions *) exception NoCoercion @@ -424,7 +420,7 @@ let inh_app_fun resolve_tc env evd j = try inh_app_fun_core env evd j with | NoCoercion when not resolve_tc - || not !use_typeclasses_for_conversion -> (evd, j) + || not (get_use_typeclasses_for_conversion ()) -> (evd, j) | NoCoercion -> try inh_app_fun_core env (saturate_evd env evd) j with NoCoercion -> (evd, j) @@ -534,7 +530,7 @@ let inh_conv_coerce_to_gen ?loc resolve_tc rigidonly env evd cj t = coerce_itf ?loc env evd (Some cj.uj_val) cj.uj_type t else raise NoSubtacCoercion with - | NoSubtacCoercion when not resolve_tc || not !use_typeclasses_for_conversion -> + | NoSubtacCoercion when not resolve_tc || not (get_use_typeclasses_for_conversion ()) -> error_actual_type ?loc env best_failed_evd cj t e | NoSubtacCoercion -> let evd' = saturate_evd env evd in diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 3391750209..f5e48bcd39 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -105,16 +105,12 @@ let search_guard ?loc env possible_indexes fixdefs = (* To force universe name declaration before use *) -let strict_universe_declarations = ref true -let is_strict_universe_declarations () = !strict_universe_declarations - -let () = - Goptions.(declare_bool_option - { optdepr = false; - optname = "strict universe declaration"; - optkey = ["Strict";"Universe";"Declaration"]; - optread = is_strict_universe_declarations; - optwrite = (:=) strict_universe_declarations }) +let is_strict_universe_declarations = + Goptions.declare_bool_option_and_ref + ~depr:false + ~name:"strict universe declaration" + ~key:["Strict";"Universe";"Declaration"] + ~value:true (** Miscellaneous interpretation functions *) diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index c68890a87f..d732544c5c 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -31,19 +31,12 @@ type 'a hint_info_gen = type hint_info = (Pattern.patvar list * Pattern.constr_pattern) hint_info_gen -let typeclasses_unique_solutions = ref false -let set_typeclasses_unique_solutions d = (:=) typeclasses_unique_solutions d -let get_typeclasses_unique_solutions () = !typeclasses_unique_solutions - -open Goptions - -let () = - declare_bool_option - { optdepr = false; - optname = "check that typeclasses proof search returns unique solutions"; - optkey = ["Typeclasses";"Unique";"Solutions"]; - optread = get_typeclasses_unique_solutions; - optwrite = set_typeclasses_unique_solutions; } +let get_typeclasses_unique_solutions = + Goptions.declare_bool_option_and_ref + ~depr:false + ~name:"check that typeclasses proof search returns unique solutions" + ~key:["Typeclasses";"Unique";"Solutions"] + ~value:false let (add_instance_hint, add_instance_hint_hook) = Hook.make () let add_instance_hint id = Hook.get add_instance_hint id @@ -434,28 +427,40 @@ let remove_instance i = Lib.add_anonymous_leaf (instance_input (RemoveInstance, i)); remove_instance_hint i.is_impl -let declare_instance info local glob = +let warning_not_a_class = + let name = "not-a-class" in + let category = "typeclasses" in + CWarnings.create ~name ~category (fun (n, ty) -> + let env = Global.env () in + let evd = Evd.from_env env in + Pp.(str "Ignored instance declaration for “" + ++ Nametab.pr_global_env Id.Set.empty n + ++ str "”: “" + ++ Termops.Internal.print_constr_env env evd (EConstr.of_constr ty) + ++ str "” is not a class") + ) + +let declare_instance ?(warn = false) info local glob = let ty, _ = Typeops.type_of_global_in_context (Global.env ()) glob in let info = Option.default {hint_priority = None; hint_pattern = None} info in match class_of_constr Evd.empty (EConstr.of_constr ty) with | Some (rels, ((tc,_), args) as _cl) -> assert (not (isVarRef glob) || local); add_instance (new_instance tc info (not local) glob) - | None -> () + | None -> if warn then warning_not_a_class (glob, ty) let add_class cl = add_class cl; List.iter (fun (n, inst, body) -> - match inst with - | Some (Backward, info) -> - (match body with - | None -> CErrors.user_err Pp.(str "Non-definable projection can not be declared as a subinstance") - | Some b -> declare_instance (Some info) false (ConstRef b)) - | _ -> ()) - cl.cl_projs + match inst with + | Some (Backward, info) -> + (match body with + | None -> CErrors.user_err Pp.(str "Non-definable projection can not be declared as a subinstance") + | Some b -> declare_instance ~warn:true (Some info) false (ConstRef b)) + | _ -> ()) + cl.cl_projs - (* * interface functions *) diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli index 8bdac0a575..d00195678b 100644 --- a/pretyping/typeclasses.mli +++ b/pretyping/typeclasses.mli @@ -133,7 +133,10 @@ val remove_instance_hint : GlobRef.t -> unit val solve_all_instances_hook : (env -> evar_map -> evar_filter -> bool -> bool -> bool -> evar_map) Hook.t val solve_one_instance_hook : (env -> evar_map -> EConstr.types -> bool -> evar_map * EConstr.constr) Hook.t -val declare_instance : hint_info option -> bool -> GlobRef.t -> unit +(** Declares the given global reference as an instance of its type. + Does nothing — or emit a “not-a-class” warning if the [warn] argument is set — + when said type is not a registered type class. *) +val declare_instance : ?warn:bool -> hint_info option -> bool -> GlobRef.t -> unit (** Build the subinstances hints for a given typeclass object. diff --git a/stm/stm.ml b/stm/stm.ml index c078dbae56..94405924b7 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2838,13 +2838,12 @@ let process_back_meta_command ~newtip ~head oid aast w = VCS.commit id (Alias (oid,aast)); Backtrack.record (); if w == VtNow then ignore(finish ~doc:dummy_doc); `Ok -let allow_nested_proofs = ref false -let () = Goptions.(declare_bool_option - { optdepr = false; - optname = "Nested Proofs Allowed"; - optkey = Vernac_classifier.stm_allow_nested_proofs_option_name; - optread = (fun () -> !allow_nested_proofs); - optwrite = (fun b -> allow_nested_proofs := b) }) +let get_allow_nested_proofs = + Goptions.declare_bool_option_and_ref + ~depr:false + ~name:"Nested Proofs Allowed" + ~key:Vernac_classifier.stm_allow_nested_proofs_option_name + ~value:false let process_transaction ~doc ?(newtip=Stateid.fresh ()) ({ verbose; loc; expr } as x) c = @@ -2877,7 +2876,7 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ()) (* Proof *) | VtStartProof (mode, guarantee, names), w -> - if not !allow_nested_proofs && VCS.proof_nesting () > 0 then + if not (get_allow_nested_proofs ()) && VCS.proof_nesting () > 0 then "Nested proofs are not allowed unless you turn option Nested Proofs Allowed on." |> Pp.str |> (fun s -> (UserError (None, s), Exninfo.null)) diff --git a/test-suite/bugs/closed/bug_9014.v b/test-suite/bugs/closed/bug_9014.v new file mode 100644 index 0000000000..c1fdd04a65 --- /dev/null +++ b/test-suite/bugs/closed/bug_9014.v @@ -0,0 +1,19 @@ +(* A type, not a class *) +Variant T := mkT. + +(* In records, :> declares a coercion *) +Record R := { t_of_r :> T }. +Check forall r : R, r = r :> T. + +(* A class *) +Class A := { p : Prop }. +(* A sub-class *) +Class B := { a_of_b :> A ; t_of_b :> T }. +(* The sub-instance is automatically inferred due to :> for a_of_b *) +Check forall b : B, p. +(* No coercion is introduced by :> in t_of_b *) +Fail Check forall b : B, b = b :> T. + +(* Using :> when the RHS is not a class produces a “not-a-class” warning. *) +Set Warnings "+not-a-class". +Fail Class B' := { a_of_b' :> A ; t_of_b' :> T }. diff --git a/theories/Structures/OrdersFacts.v b/theories/Structures/OrdersFacts.v index 60c64d306b..1fb0a37e16 100644 --- a/theories/Structures/OrdersFacts.v +++ b/theories/Structures/OrdersFacts.v @@ -77,7 +77,7 @@ End CompareFacts. (** * Properties of [OrderedTypeFull] *) -Module Type OrderedTypeFullFacts (Import O:OrderedTypeFull'). +Module OrderedTypeFullFacts (Import O:OrderedTypeFull'). Module OrderTac := OTF_to_OrderTac O. Ltac order := OrderTac.order. diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml index b98535b201..6c4ea9afa1 100644 --- a/toplevel/coqargs.ml +++ b/toplevel/coqargs.ml @@ -91,7 +91,7 @@ type coq_cmdopts = { let default_toplevel = Names.(DirPath.make [Id.of_string "Top"]) -let init_args = { +let default_opts = { load_init = true; load_rcfile = true; @@ -139,6 +139,8 @@ let init_args = { print_emacs = false; + (* Quiet / verbosity options should be here *) + inputstate = None; outputstate = None; } @@ -166,6 +168,7 @@ let add_compat_require opts v = | Flags.Current -> add_vo_require opts "Coq.Compat.Coq89" None (Some false) let set_batch_mode opts = + (* XXX: This should be in the argument record *) Flags.quiet := true; System.trust_file_cache := true; { opts with batch_mode = true } @@ -281,11 +284,6 @@ let get_cache opt = function | "force" -> Some Stm.AsyncOpts.Force | _ -> prerr_endline ("Error: force expected after "^opt); exit 1 -let get_identifier opt s = - try Names.Id.of_string s - with CErrors.UserError _ -> - prerr_endline ("Error: valid identifier expected after option "^opt); exit 1 - let is_not_dash_option = function | Some f when String.length f > 0 && f.[0] <> '-' -> true | _ -> false @@ -325,7 +323,7 @@ let usage batch = else Usage.print_usage_coqtop () (* Main parsing routine *) -let parse_args arglist : coq_cmdopts * string list = +let parse_args init_opts arglist : coq_cmdopts * string list = let args = ref arglist in let extras = ref [] in let rec parse oval = match !args with @@ -478,7 +476,9 @@ let parse_args arglist : coq_cmdopts * string list = add_load_vernacular oval true (next ()) |"-mangle-names" -> - Namegen.set_mangle_names_mode (get_identifier opt (next ())); oval + Goptions.set_bool_option_value ["Mangle"; "Names"] true; + Goptions.set_string_option_value ["Mangle"; "Names"; "Prefix"] (next ()); + oval |"-print-mod-uid" -> let s = String.concat " " (List.map get_native_name rem) in print_endline s; exit 0 @@ -596,7 +596,7 @@ let parse_args arglist : coq_cmdopts * string list = parse noval in try - parse init_args + parse init_opts with any -> fatal_error any (******************************************************************************) diff --git a/toplevel/coqargs.mli b/toplevel/coqargs.mli index 30f1caab12..e645b0c126 100644 --- a/toplevel/coqargs.mli +++ b/toplevel/coqargs.mli @@ -63,12 +63,17 @@ type coq_cmdopts = { print_emacs : bool; + (* Quiet / verbosity options should be here *) + inputstate : string option; outputstate : string option; } -val parse_args : string list -> coq_cmdopts * string list +(* Default options *) +val default_opts : coq_cmdopts + +val parse_args : coq_cmdopts -> string list -> coq_cmdopts * string list val exitcode : coq_cmdopts -> int val require_libs : coq_cmdopts -> (string * string option * bool option) list diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index faacbe4c80..edef741ca6 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -148,7 +148,7 @@ let init_gc () = Gc.space_overhead = 120} (** Main init routine *) -let init_toplevel custom_init arglist = +let init_toplevel init_opts custom_init arglist = (* Coq's init process, phase 1: OCaml parameters, basic structures, and IO *) @@ -164,7 +164,7 @@ let init_toplevel custom_init arglist = *) let res = begin try - let opts,extras = parse_args arglist in + let opts,extras = parse_args init_opts arglist in memory_stat := opts.memory_stat; (* If we have been spawned by the Spawn module, this has to be done @@ -252,20 +252,25 @@ let init_toplevel custom_init arglist = Feedback.del_feeder init_feeder; res -type custom_toplevel = { - init : opts:coq_cmdopts -> string list -> coq_cmdopts * string list; - run : opts:coq_cmdopts -> state:Vernac.State.t -> unit; -} +type custom_toplevel = + { init : opts:coq_cmdopts -> string list -> coq_cmdopts * string list + ; run : opts:coq_cmdopts -> state:Vernac.State.t -> unit + ; opts : Coqargs.coq_cmdopts + } let coqtop_init ~opts extra = init_color opts; CoqworkmgrApi.(init !async_proofs_worker_priority); opts, extra -let coqtop_toplevel = { init = coqtop_init; run = Coqloop.loop; } +let coqtop_toplevel = + { init = coqtop_init + ; run = Coqloop.loop + ; opts = Coqargs.default_opts + } let start_coq custom = - match init_toplevel custom.init (List.tl (Array.to_list Sys.argv)) with + match init_toplevel custom.opts custom.init (List.tl (Array.to_list Sys.argv)) with (* Batch mode *) | Some state, opts when not opts.batch_mode -> custom.run ~opts ~state; diff --git a/toplevel/coqtop.mli b/toplevel/coqtop.mli index 641448f10a..c95d0aca55 100644 --- a/toplevel/coqtop.mli +++ b/toplevel/coqtop.mli @@ -12,10 +12,13 @@ [init] is used to do custom command line argument parsing. [run] launches a custom toplevel. *) -type custom_toplevel = { - init : opts:Coqargs.coq_cmdopts -> string list -> Coqargs.coq_cmdopts * string list; - run : opts:Coqargs.coq_cmdopts -> state:Vernac.State.t -> unit; -} +open Coqargs + +type custom_toplevel = + { init : opts:coq_cmdopts -> string list -> coq_cmdopts * string list + ; run : opts:coq_cmdopts -> state:Vernac.State.t -> unit + ; opts : Coqargs.coq_cmdopts + } val coqtop_toplevel : custom_toplevel diff --git a/toplevel/workerLoop.ml b/toplevel/workerLoop.ml index ee6d5e8843..e4e9a87365 100644 --- a/toplevel/workerLoop.ml +++ b/toplevel/workerLoop.ml @@ -23,6 +23,7 @@ let arg_init init ~opts extra_args = let start ~init ~loop = let open Coqtop in let custom = { + opts = Coqargs.default_opts; init = arg_init init; run = (fun ~opts:_ ~state:_ -> loop ()); } in diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml index 16101396cf..43abc0a200 100644 --- a/vernac/egramcoq.ml +++ b/vernac/egramcoq.ml @@ -33,24 +33,24 @@ open Pcoq let constr_level = string_of_int let default_levels = - [200,Extend.RightA,false; - 100,Extend.RightA,false; - 99,Extend.RightA,true; - 90,Extend.RightA,true; - 10,Extend.LeftA,false; - 9,Extend.RightA,false; - 8,Extend.RightA,true; - 1,Extend.LeftA,false; - 0,Extend.RightA,false] + [200,Gramlib.Gramext.RightA,false; + 100,Gramlib.Gramext.RightA,false; + 99,Gramlib.Gramext.RightA,true; + 90,Gramlib.Gramext.RightA,true; + 10,Gramlib.Gramext.LeftA,false; + 9,Gramlib.Gramext.RightA,false; + 8,Gramlib.Gramext.RightA,true; + 1,Gramlib.Gramext.LeftA,false; + 0,Gramlib.Gramext.RightA,false] let default_pattern_levels = - [200,Extend.RightA,true; - 100,Extend.RightA,false; - 99,Extend.RightA,true; - 90,Extend.RightA,true; - 10,Extend.LeftA,false; - 1,Extend.LeftA,false; - 0,Extend.RightA,false] + [200,Gramlib.Gramext.RightA,true; + 100,Gramlib.Gramext.RightA,false; + 99,Gramlib.Gramext.RightA,true; + 90,Gramlib.Gramext.RightA,true; + 10,Gramlib.Gramext.LeftA,false; + 1,Gramlib.Gramext.LeftA,false; + 0,Gramlib.Gramext.RightA,false] let default_constr_levels = (default_levels, default_pattern_levels) @@ -70,28 +70,28 @@ let save_levels levels custom lev = (* first LeftA, then RightA and NoneA together *) let admissible_assoc = function - | Extend.LeftA, Some (Extend.RightA | Extend.NonA) -> false - | Extend.RightA, Some Extend.LeftA -> false + | Gramlib.Gramext.LeftA, Some (Gramlib.Gramext.RightA | Gramlib.Gramext.NonA) -> false + | Gramlib.Gramext.RightA, Some Gramlib.Gramext.LeftA -> false | _ -> true let create_assoc = function - | None -> Extend.RightA + | None -> Gramlib.Gramext.RightA | Some a -> a let error_level_assoc p current expected = let open Pp in let pr_assoc = function - | Extend.LeftA -> str "left" - | Extend.RightA -> str "right" - | Extend.NonA -> str "non" in + | Gramlib.Gramext.LeftA -> str "left" + | Gramlib.Gramext.RightA -> str "right" + | Gramlib.Gramext.NonA -> str "non" in user_err (str "Level " ++ int p ++ str " is already declared " ++ pr_assoc current ++ str " associative while it is now expected to be " ++ pr_assoc expected ++ str " associative.") let create_pos = function - | None -> Extend.First - | Some lev -> Extend.After (constr_level lev) + | None -> Gramlib.Gramext.First + | Some lev -> Gramlib.Gramext.After (constr_level lev) let find_position_gen current ensure assoc lev = match lev with @@ -121,13 +121,13 @@ let find_position_gen current ensure assoc lev = updated, (Some (create_pos !after), Some assoc, Some (constr_level n), None) | _ -> (* The reinit flag has been updated *) - updated, (Some (Extend.Level (constr_level n)), None, None, !init) + updated, (Some (Gramlib.Gramext.Level (constr_level n)), None, None, !init) end with (* Nothing has changed *) Exit -> (* Just inherit the existing associativity and name (None) *) - current, (Some (Extend.Level (constr_level n)), None, None, None) + current, (Some (Gramlib.Gramext.Level (constr_level n)), None, None, None) let rec list_mem_assoc_triple x = function | [] -> false @@ -186,15 +186,18 @@ let find_position accu custom forpat assoc level = (* Binding constr entry keys to entries *) (* Camlp5 levels do not treat NonA: use RightA with a NEXT on the left *) -let camlp5_assoc = function - | Some NonA | Some RightA -> RightA - | None | Some LeftA -> LeftA - -let assoc_eq al ar = match al, ar with -| NonA, NonA -| RightA, RightA -| LeftA, LeftA -> true -| _, _ -> false +let camlp5_assoc = + let open Gramlib.Gramext in function + | Some NonA | Some RightA -> RightA + | None | Some LeftA -> LeftA + +let assoc_eq al ar = + let open Gramlib.Gramext in + match al, ar with + | NonA, NonA + | RightA, RightA + | LeftA, LeftA -> true + | _, _ -> false (* [adjust_level assoc from prod] where [assoc] and [from] are the name and associativity of the level where to add the rule; the meaning of @@ -204,7 +207,7 @@ let assoc_eq al ar = match al, ar with Some None = NEXT Some (Some (n,cur)) = constr LEVEL n s.t. if [cur] is set then [n] is the same as the [from] level *) -let adjust_level assoc from = function +let adjust_level assoc from = let open Gramlib.Gramext in function (* Associativity is None means force the level *) | (NumLevel n,BorderProd (_,None)) -> Some (Some (n,true)) (* Compute production name on the right side *) diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index e3f6a87541..22528a607f 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -1175,9 +1175,9 @@ GRAMMAR EXTEND Gram | "in"; IDENT "custom"; x = IDENT -> { SetCustomEntry (x,None) } | "in"; IDENT "custom"; x = IDENT; "at"; IDENT "level"; n = natural -> { SetCustomEntry (x,Some n) } - | IDENT "left"; IDENT "associativity" -> { SetAssoc LeftA } - | IDENT "right"; IDENT "associativity" -> { SetAssoc RightA } - | IDENT "no"; IDENT "associativity" -> { SetAssoc NonA } + | IDENT "left"; IDENT "associativity" -> { SetAssoc Gramlib.Gramext.LeftA } + | IDENT "right"; IDENT "associativity" -> { SetAssoc Gramlib.Gramext.RightA } + | IDENT "no"; IDENT "associativity" -> { SetAssoc Gramlib.Gramext.NonA } | IDENT "only"; IDENT "printing" -> { SetOnlyPrinting } | IDENT "only"; IDENT "parsing" -> { SetOnlyParsing } | IDENT "compat"; s = STRING -> diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index 5ab877fae2..82434afbbd 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -287,7 +287,7 @@ let pr_notation_entry = function | InConstrEntry -> str "constr" | InCustomEntry s -> str "custom " ++ str s -let prec_assoc = function +let prec_assoc = let open Gramlib.Gramext in function | RightA -> (L,E) | LeftA -> (E,L) | NonA -> (L,L) @@ -685,7 +685,7 @@ let border = function | (_,(ETConstr(_,_,(_,BorderProd (_,a))))) :: _ -> a | _ -> None -let recompute_assoc typs = +let recompute_assoc typs = let open Gramlib.Gramext in match border typs, border (List.rev typs) with | Some LeftA, Some RightA -> assert false | Some LeftA, _ -> Some LeftA @@ -802,7 +802,7 @@ let inSyntaxExtension : syntax_extension_obj -> obj = module NotationMods = struct type notation_modifier = { - assoc : gram_assoc option; + assoc : Gramlib.Gramext.g_assoc option; level : int option; custom : notation_entry; etyps : (Id.t * simple_constr_prod_entry_key) list; @@ -1230,7 +1230,7 @@ let compute_syntax_data local df modifiers = let onlyprint = mods.only_printing in let onlyparse = mods.only_parsing in if onlyprint && onlyparse then user_err (str "A notation cannot be both 'only printing' and 'only parsing'."); - let assoc = Option.append mods.assoc (Some NonA) in + let assoc = Option.append mods.assoc (Some Gramlib.Gramext.NonA) in let (recvars,mainvars,symbols) = analyze_notation_tokens ~onlyprint df in let _ = check_useless_entry_types recvars mainvars mods.etyps in let _ = check_binder_type recvars mods.etyps in diff --git a/vernac/obligations.ml b/vernac/obligations.ml index cbb77057bd..4926b8c3e1 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -337,32 +337,20 @@ let assumption_message = Declare.assumption_message let default_tactic = ref (Proofview.tclUNIT ()) (* true = hide obligations *) -let hide_obligations = ref false - -let set_hide_obligations = (:=) hide_obligations -let get_hide_obligations () = !hide_obligations - -open Goptions -let () = - declare_bool_option - { optdepr = false; - optname = "Hiding of Program obligations"; - optkey = ["Hide";"Obligations"]; - optread = get_hide_obligations; - optwrite = set_hide_obligations; } - -let shrink_obligations = ref true - -let set_shrink_obligations = (:=) shrink_obligations -let get_shrink_obligations () = !shrink_obligations - -let () = - declare_bool_option - { optdepr = true; (* remove in 8.8 *) - optname = "Shrinking of Program obligations"; - optkey = ["Shrink";"Obligations"]; - optread = get_shrink_obligations; - optwrite = set_shrink_obligations; } +let get_hide_obligations = + Goptions.declare_bool_option_and_ref + ~depr:false + ~name:"Hidding of Program obligations" + ~key:["Hide";"Obligations"] + ~value:false + + +let get_shrink_obligations = + Goptions.declare_bool_option_and_ref + ~depr:true (* remove in 8.8 *) + ~name:"Shrinking of Program obligations" + ~key:["Shrink";"Obligations"] + ~value:true let evar_of_obligation o = make_evar (Global.named_context_val ()) (EConstr.of_constr o.obl_type) diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index 2ddd210365..e7c1e29beb 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -380,7 +380,7 @@ open Pputils let pr_thm_token k = keyword (Kindops.string_of_theorem_kind k) - let pr_syntax_modifier = function + let pr_syntax_modifier = let open Gramlib.Gramext in function | SetItemLevel (l,bko,n) -> prlist_with_sep sep_v2 str l ++ spc () ++ pr_at_level_opt n ++ pr_opt pr_constr_as_binder_kind bko diff --git a/vernac/record.ml b/vernac/record.ml index 81b33c2e11..f6dbcb5291 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -458,7 +458,7 @@ let implicits_of_context ctx = in ExplByPos (i, explname), (true, true, true)) 1 (List.rev (Anonymous :: (List.map RelDecl.get_name ctx))) -let declare_class finite def cum ubinders univs id idbuild paramimpls params arity +let declare_class def cum ubinders univs id idbuild paramimpls params arity template fieldimpls fields ?(kind=StructureComponent) coers priorities = let fieldimpls = (* Make the class implicit in the projections, and the params if applicable. *) @@ -671,7 +671,7 @@ let definition_structure udecl kind ~template cum poly finite records = in let priorities = List.map (fun ((_, id), _) -> {hint_priority = id; hint_pattern = None}) cfs in let coers = List.map (fun (((coe, _), _), _) -> coe) cfs in - declare_class finite def cum ubinders univs id.CAst.v idbuild + declare_class def cum ubinders univs id.CAst.v idbuild implpars params arity template implfs fields coers priorities | _ -> let map impls = implpars @ Impargs.lift_implicits (succ (List.length params)) impls in diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index fa1082473e..a157e01fc1 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -582,10 +582,15 @@ let should_treat_as_cumulative cum poly = else user_err Pp.(str "The NonCumulative prefix can only be used in a polymorphic context.") | None -> poly && Flags.is_polymorphic_inductive_cumulativity () -let uniform_inductive_parameters = ref false +let get_uniform_inductive_parameters = + Goptions.declare_bool_option_and_ref + ~depr:false + ~name:"Uniform inductive parameters" + ~key:["Uniform"; "Inductive"; "Parameters"] + ~value:false let should_treat_as_uniform () = - if !uniform_inductive_parameters + if get_uniform_inductive_parameters () then ComInductive.UniformParameters else ComInductive.NonUniformParameters @@ -1538,14 +1543,6 @@ let () = optwrite = Flags.make_polymorphic_inductive_cumulativity } let () = - declare_bool_option - { optdepr = false; - optname = "Uniform inductive parameters"; - optkey = ["Uniform"; "Inductive"; "Parameters"]; - optread = (fun () -> !uniform_inductive_parameters); - optwrite = (fun b -> uniform_inductive_parameters := b) } - -let () = declare_int_option { optdepr = false; optname = "the level of inlining during functor application"; diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index 122005e011..1e6c40c829 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -167,7 +167,7 @@ type syntax_modifier = | SetItemLevel of string list * Notation_term.constr_as_binder_kind option * Extend.production_level option | SetLevel of int | SetCustomEntry of string * int option - | SetAssoc of Extend.gram_assoc + | SetAssoc of Gramlib.Gramext.g_assoc | SetEntryType of string * Extend.simple_constr_prod_entry_key | SetOnlyParsing | SetOnlyPrinting |