diff options
130 files changed, 1125 insertions, 953 deletions
@@ -170,6 +170,7 @@ of the Coq Proof assistant during the indicated time: Nickolai Zeldovich (MIT 2014-2016) Théo Zimmermann (ORCID: https://orcid.org/0000-0002-3580-8806, INRIA-PPS then IRIF, 2015-now) + Talia Ringer (UW, 2019) *************************************************************************** INRIA refers to: diff --git a/dev/ci/user-overlays/09895-ejgallego-require+upper.sh b/dev/ci/user-overlays/09895-ejgallego-require+upper.sh new file mode 100644 index 0000000000..9a42c829ce --- /dev/null +++ b/dev/ci/user-overlays/09895-ejgallego-require+upper.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "9895" ] || [ "$CI_BRANCH" = "require+upper" ]; then + + quickchick_CI_REF=require+upper + quickchick_CI_GITURL=https://github.com/ejgallego/QuickChick + +fi diff --git a/dev/ci/user-overlays/10185-SkySkimmer-instance-no-bang.sh b/dev/ci/user-overlays/10185-SkySkimmer-instance-no-bang.sh new file mode 100644 index 0000000000..c584438b21 --- /dev/null +++ b/dev/ci/user-overlays/10185-SkySkimmer-instance-no-bang.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "10185" ] || [ "$CI_BRANCH" = "instance-no-bang" ]; then + + quickchick_CI_REF=instance-no-bang + quickchick_CI_GITURL=https://github.com/SkySkimmer/QuickChick + +fi diff --git a/dev/doc/build-system.dev.txt b/dev/doc/build-system.dev.txt index 6efc8ec1fe..6bbf83aa7e 100644 --- a/dev/doc/build-system.dev.txt +++ b/dev/doc/build-system.dev.txt @@ -88,7 +88,7 @@ Cons: Makefiles hierarchy ------------------- +------------------- The Makefile is separated in several files : @@ -101,7 +101,7 @@ The Makefile is separated in several files : FIND_SKIP_DIRS ---------------- +-------------- The recommended style of using FIND_SKIP_DIRS is for example diff --git a/dev/doc/build-system.dune.md b/dev/doc/build-system.dune.md index 49251d61a1..372e40a0b7 100644 --- a/dev/doc/build-system.dune.md +++ b/dev/doc/build-system.dune.md @@ -108,14 +108,14 @@ automatically. You can use `ocamldebug` with Dune; after a build, do: ``` -dune exec dev/dune-dbg +dune exec dev/dune-dbg /path/to/foo.v (ocd) source dune_db ``` or ``` -dune exec dev/dune-dbg checker +dune exec dev/dune-dbg checker Foo (ocd) source dune_db ``` @@ -124,6 +124,8 @@ refined, so you need to build enough of Coq once to use this target [it will then correctly compute the deps and rebuild if you call the script again] This will be fixed in the future. +For running in emacs, use `coqdev-ocamldebug` from `coqdev.el`. + ## Dropping from coqtop: After doing `make -f Makefile.dune voboot`, the following commands should work: @@ -3,7 +3,7 @@ (public_name coq.top_printers) (synopsis "Coq's Debug Printers") (wrapped false) - (modules :standard) + (modules top_printers) (optional) (libraries coq.toplevel coq.plugins.ltac)) @@ -11,7 +11,7 @@ (targets dune-dbg) (deps dune-dbg.in ../checker/coqchk.bc - ../topbin/coqtop_byte_bin.bc + ../topbin/coqc_bin.bc ; This is not enough as the call to `ocamlfind` will fail :/ top_printers.cma) (action (copy dune-dbg.in dune-dbg))) diff --git a/dev/dune-dbg.in b/dev/dune-dbg.in index 80ad0500e0..bd0a837938 100755 --- a/dev/dune-dbg.in +++ b/dev/dune-dbg.in @@ -3,11 +3,14 @@ # Run in a proper install dune env. case $1 in checker) + shift exe=_build/default/checker/coqchk.bc ;; *) - exe=_build/default/topbin/coqtop_byte_bin.bc + exe=_build/default/topbin/coqc_bin.bc ;; esac -ocamldebug $(ocamlfind query -recursive -i-format coq.top_printers) -I +threads -I dev $exe +emacs="${INSIDE_EMACS:+-emacs}" + +ocamldebug $emacs $(ocamlfind query -recursive -i-format coq.top_printers) -I +threads -I dev $exe "$@" diff --git a/dev/tools/coqdev.el b/dev/tools/coqdev.el index c6687b9731..b89ae67a82 100644 --- a/dev/tools/coqdev.el +++ b/dev/tools/coqdev.el @@ -85,6 +85,35 @@ Note that this function is executed before _Coqproject is read if it exists." (setq-local coq-prog-name (concat dir "bin/coqtop"))))) (add-hook 'hack-local-variables-hook #'coqdev-setup-proofgeneral) +(defvar coqdev-ocamldebug-command "dune exec dev/dune-dbg" + "Command run by `coqdev-ocamldebug'") + +(defun coqdev-ocamldebug () + "Runs a command in an ocamldebug buffer." + (interactive) + (let* ((dir (read-directory-name "Run from directory: " + (coqdev-default-directory))) + (name "ocamldebug-coq") + (buffer-name (concat "*" name "*"))) + (pop-to-buffer buffer-name) + (unless (comint-check-proc buffer-name) + (setq default-directory dir) + (setq coqdev-ocamldebug-command + (read-from-minibuffer "Command to run: " + coqdev-ocamldebug-command)) + (let* ((cmdlist (tuareg--split-args coqdev-ocamldebug-command)) + (cmdlist (mapcar #'substitute-in-file-name cmdlist))) + (apply #'make-comint name + (car cmdlist) + nil + (cdr cmdlist)) + (set-process-filter (get-buffer-process (current-buffer)) + #'ocamldebug-filter) + (set-process-sentinel (get-buffer-process (current-buffer)) + #'ocamldebug-sentinel) + (ocamldebug-mode))) + (ocamldebug-set-buffer))) + ;; This Elisp snippet adds a regexp parser for the format of Anomaly ;; backtraces (coqc -bt ...), to the error parser of the Compilation ;; mode (C-c C-c: "Compile command: ..."). File locations in traces diff --git a/doc/changelog/02-specification-language/10167-orpat-mixfix.rst b/doc/changelog/02-specification-language/10167-orpat-mixfix.rst new file mode 100644 index 0000000000..e3c3923348 --- /dev/null +++ b/doc/changelog/02-specification-language/10167-orpat-mixfix.rst @@ -0,0 +1,12 @@ +- Require parentheses around nested disjunctive patterns, so that pattern and + term syntax are consistent; match branch patterns no longer require + parentheses for notation at level 100 or more. Incompatibilities: + + + in :g:`match p with (_, (0|1)) => ...` parentheses may no longer be + omitted around :n:`0|1`. + + notation :g:`(p | q)` now potentially clashes with core pattern syntax, + and should be avoided. ``-w disj-pattern-notation`` flags such :cmd:`Notation`. + + see :ref:`extendedpatternmatching` for details + (`#10167 <https://github.com/coq/coq/pull/10167>`_, + by Georges Gonthier). diff --git a/doc/changelog/07-commands-and-options/10185-instance-no-bang.rst b/doc/changelog/07-commands-and-options/10185-instance-no-bang.rst new file mode 100644 index 0000000000..c69cda9656 --- /dev/null +++ b/doc/changelog/07-commands-and-options/10185-instance-no-bang.rst @@ -0,0 +1,2 @@ +- Remove undocumented :n:`Instance : !@type` syntax + (`#10185 <https://github.com/coq/coq/pull/10185>`_, by Gaëtan Gilbert). diff --git a/doc/sphinx/addendum/extended-pattern-matching.rst b/doc/sphinx/addendum/extended-pattern-matching.rst index e882ce6e88..b568160356 100644 --- a/doc/sphinx/addendum/extended-pattern-matching.rst +++ b/doc/sphinx/addendum/extended-pattern-matching.rst @@ -21,10 +21,10 @@ type is considered to be a variable. A variable name cannot occur more than once in a given pattern. It is recommended to start variable names by a lowercase letter. -If a pattern has the form ``(c x)`` where ``c`` is a constructor symbol and x +If a pattern has the form ``c x`` where ``c`` is a constructor symbol and x is a linear vector of (distinct) variables, it is called *simple*: it is the kind of pattern recognized by the basic version of match. On -the opposite, if it is a variable ``x`` or has the form ``(c p)`` with ``p`` not +the opposite, if it is a variable ``x`` or has the form ``c p`` with ``p`` not only made of variables, the pattern is called *nested*. A variable pattern matches any value, and the identifier is bound to @@ -216,7 +216,8 @@ Here is an example: end. -Here is another example using disjunctive subpatterns. +Nested disjunctive patterns are allowed, inside parentheses, with the +notation :n:`({+| @pattern})`, as in: .. coqtop:: in diff --git a/doc/sphinx/addendum/generalized-rewriting.rst b/doc/sphinx/addendum/generalized-rewriting.rst index 68f6d4008a..e58049b8d0 100644 --- a/doc/sphinx/addendum/generalized-rewriting.rst +++ b/doc/sphinx/addendum/generalized-rewriting.rst @@ -528,7 +528,7 @@ pass additional arguments such as ``using relation``. .. tacv:: setoid_reflexivity setoid_symmetry {? in @ident} setoid_transitivity - setoid_rewrite {? @orientation} @term {? at @occs} {? in @ident} + setoid_rewrite {? @orientation} @term {? at @occurrences} {? in @ident} setoid_replace @term with @term {? using relation @term} {? in @ident} {? by @tactic} :name: setoid_reflexivity; setoid_symmetry; setoid_transitivity; setoid_rewrite; setoid_replace @@ -567,13 +567,13 @@ Printing relations and morphisms Deprecated syntax and backward incompatibilities ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -.. cmd:: Add Setoid @A @Aeq @ST as @ident +.. cmd:: Add Setoid @qualid__1 @qualid__2 @qualid__3 as @ident This command for declaring setoids and morphisms is also accepted due to backward compatibility reasons. - Here ``Aeq`` is a congruence relation without parameters, ``A`` is its carrier - and ``ST`` is an object of type (``Setoid_Theory A Aeq``) (i.e. a record + Here :n:`@qualid__2` is a congruence relation without parameters, :n:`@qualid__1` is its carrier + and :n:`@qualid__3` is an object of type (:n:`Setoid_Theory @qualid__1 @qualid__2`) (i.e. a record packing together the reflexivity, symmetry and transitivity lemmas). Notice that the syntax is not completely backward compatible since the identifier was not required. @@ -708,91 +708,65 @@ Definitions The generalized rewriting tactic is based on a set of strategies that can be combined to obtain custom rewriting procedures. Its set of strategies is based on Elan’s rewriting strategies :cite:`Luttik97specificationof`. Rewriting -strategies are applied using the tactic ``rewrite_strat s`` where ``s`` is a +strategies are applied using the tactic :n:`rewrite_strat @strategy` where :token:`strategy` is a strategy expression. Strategies are defined inductively as described by the following grammar: -.. productionlist:: rewriting - s, t, u : `strategy` - : `lemma` - : `lemma_right_to_left` - : `failure` - : `identity` - : `reflexivity` - : `progress` - : `failure_catch` - : `composition` - : `left_biased_choice` - : `iteration_one_or_more` - : `iteration_zero_or_more` - : `one_subterm` - : `all_subterms` - : `innermost_first` - : `outermost_first` - : `bottom_up` - : `top_down` - : `apply_hint` - : `any_of_the_terms` - : `apply_reduction` - : `fold_expression` - -.. productionlist:: rewriting - strategy : ( `s` ) - lemma : `c` - lemma_right_to_left : <- `c` - failure : fail - identity : id - reflexivity : refl - progress : progress `s` - failure_catch : try `s` - composition : `s` ; `u` - left_biased_choice : choice `s` `t` - iteration_one_or_more : repeat `s` - iteration_zero_or_more : any `s` - one_subterm : subterm `s` - all_subterms : subterms `s` - innermost_first : innermost `s` - outermost_first : outermost `s` - bottom_up : bottomup `s` - top_down : topdown `s` - apply_hint : hints `hintdb` - any_of_the_terms : terms (`c`)+ - apply_reduction : eval `redexpr` - fold_expression : fold `c` - +.. productionlist:: coq + strategy : `qualid` (lemma, left to right) + : <- `qualid` (lemma, right to left) + : fail (failure) + : id (identity) + : refl (reflexivity) + : progress `strategy` (progress) + : try `strategy` (try catch) + : `strategy` ; `strategy` (composition) + : choice `strategy` `strategy` (left_biased_choice) + : repeat `strategy` (one or more) + : any `strategy` (zero or more) + : subterm `strategy` (one subterm) + : subterms `strategy` (all subterms) + : innermost `strategy` (innermost first) + : outermost `strategy` (outermost first) + : bottomup `strategy` (bottom-up) + : topdown `strategy` (top-down) + : hints `ident` (apply hints from hint database) + : terms `term` ... `term` (any of the terms) + : eval `redexpr` (apply reduction) + : fold `term` (unify) + : ( `strategy` ) Actually a few of these are defined in term of the others using a primitive fixpoint operator: -.. productionlist:: rewriting - try `s` : choice `s` `id` - any `s` : fix `u`. try (`s` ; `u`) - repeat `s` : `s` ; any `s` - bottomup s : fix `bu`. (choice (progress (subterms bu)) s) ; try bu - topdown s : fix `td`. (choice s (progress (subterms td))) ; try td - innermost s : fix `i`. (choice (subterm i) s) - outermost s : fix `o`. (choice s (subterm o)) +- :n:`try @strategy := choice @strategy id` +- :n:`any @strategy := fix @ident. try (@strategy ; @ident)` +- :n:`repeat @strategy := @strategy; any @strategy` +- :n:`bottomup @strategy := fix @ident. (choice (progress (subterms @ident)) @strategy) ; try @ident` +- :n:`topdown @strategy := fix @ident. (choice @strategy (progress (subterms @ident))) ; try @ident` +- :n:`innermost @strategy := fix @ident. (choice (subterm @ident) @strategy)` +- :n:`outermost @strategy := fix @ident. (choice @strategy (subterm @ident))` The basic control strategy semantics are straightforward: strategies are applied to subterms of the term to rewrite, starting from the root of the term. The lemma strategies unify the left-hand-side of the lemma with the current subterm and on success rewrite it to the right- hand-side. Composition can be used to continue rewriting on the -current subterm. The fail strategy always fails while the identity +current subterm. The ``fail`` strategy always fails while the identity strategy succeeds without making progress. The reflexivity strategy succeeds, making progress using a reflexivity proof of rewriting. -Progress tests progress of the argument strategy and fails if no +``progress`` tests progress of the argument :token:`strategy` and fails if no progress was made, while ``try`` always succeeds, catching failures. -Choice is left-biased: it will launch the first strategy and fall back +``choice`` is left-biased: it will launch the first strategy and fall back on the second one in case of failure. One can iterate a strategy at least 1 time using ``repeat`` and at least 0 times using ``any``. -The ``subterm`` and ``subterms`` strategies apply their argument strategy ``s`` to +The ``subterm`` and ``subterms`` strategies apply their argument :token:`strategy` to respectively one or all subterms of the current term under consideration, left-to-right. ``subterm`` stops at the first subterm for -which ``s`` made progress. The composite strategies ``innermost`` and ``outermost`` +which :token:`strategy` made progress. The composite strategies ``innermost`` and ``outermost`` perform a single innermost or outermost rewrite using their argument -strategy. Their counterparts ``bottomup`` and ``topdown`` perform as many +:token:`strategy`. Their counterparts ``bottomup`` and ``topdown`` perform as many rewritings as possible, starting from the bottom or the top of the term. @@ -802,15 +776,15 @@ lemmas at the current subterm. The ``terms`` strategy takes the lemma names directly as arguments. The ``eval`` strategy expects a reduction expression (see :ref:`performingcomputations`) and succeeds if it reduces the subterm under consideration. The ``fold`` strategy takes -a term ``c`` and tries to *unify* it to the current subterm, converting it to ``c`` -on success, it is stronger than the tactic ``fold``. +a :token:`term` and tries to *unify* it to the current subterm, converting it to :token:`term` +on success. It is stronger than the tactic ``fold``. Usage ~~~~~ -.. tacn:: rewrite_strat @s {? in @ident } +.. tacn:: rewrite_strat @strategy {? in @ident } :name: rewrite_strat Rewrite using the strategy s in hypothesis ident or the conclusion. diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst index 22ddcae584..45c74ab02a 100644 --- a/doc/sphinx/addendum/program.rst +++ b/doc/sphinx/addendum/program.rst @@ -299,9 +299,9 @@ optional tactic is replaced by the default one if not specified. Displays all remaining obligations. -.. cmd:: Obligation num {? of @ident} +.. cmd:: Obligation @num {? of @ident} - Start the proof of obligation num. + Start the proof of obligation :token:`num`. .. cmd:: Next Obligation {? of @ident} diff --git a/doc/sphinx/addendum/ring.rst b/doc/sphinx/addendum/ring.rst index 3b350d5dc0..3f4d5cc784 100644 --- a/doc/sphinx/addendum/ring.rst +++ b/doc/sphinx/addendum/ring.rst @@ -310,10 +310,10 @@ The syntax for adding a new ring is .. productionlist:: coq ring_mod : abstract | decidable `term` | morphism `term` : setoid `term` `term` - : constants [`ltac`] - : preprocess [`ltac`] - : postprocess [`ltac`] - : power_tac `term` [`ltac`] + : constants [ `tactic` ] + : preprocess [ `tactic` ] + : postprocess [ `tactic` ] + : power_tac `term` [ `tactic` ] : sign `term` : div `term` @@ -341,31 +341,31 @@ The syntax for adding a new ring is This modifier needs not be used if the setoid and morphisms have been declared. - constants [ :n:`@ltac` ] - specifies a tactic expression :n:`@ltac` that, given a + constants [ :n:`@tactic` ] + specifies a tactic expression :n:`@tactic` that, given a term, returns either an object of the coefficient set that is mapped to the expression via the morphism, or returns ``InitialRing.NotConstant``. The default behavior is to map only 0 and 1 to their counterpart in the coefficient set. This is generally not desirable for non trivial computational rings. - preprocess [ :n:`@ltac` ] - specifies a tactic :n:`@ltac` that is applied as a + preprocess [ :n:`@tactic` ] + specifies a tactic :n:`@tactic` that is applied as a preliminary step for :tacn:`ring` and :tacn:`ring_simplify`. It can be used to transform a goal so that it is better recognized. For instance, ``S n`` can be changed to ``plus 1 n``. - postprocess [ :n:`@ltac` ] - specifies a tactic :n:`@ltac` that is applied as a final + postprocess [ :n:`@tactic` ] + specifies a tactic :n:`@tactic` that is applied as a final step for :tacn:`ring_simplify`. For instance, it can be used to undo modifications of the preprocessor. - power_tac :n:`@term` [ :n:`@ltac` ] + power_tac :n:`@term` [ :n:`@tactic` ] allows :tacn:`ring` and :tacn:`ring_simplify` to recognize power expressions with a constant positive integer exponent (example: :math:`x^2` ). The term :n:`@term` is a proof that a given power function satisfies the specification of a power function (term has to be a proof of - ``Ring_theory.power_theory``) and :n:`@ltac` specifies a tactic expression + ``Ring_theory.power_theory``) and :n:`@tactic` specifies a tactic expression that, given a term, “abstracts” it into an object of type |N| whose interpretation via ``Cp_phi`` (the evaluation function of power coefficient) is the original term, or returns ``InitialRing.NotConstant`` diff --git a/doc/sphinx/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst index 1aa2111816..395b5ce2d3 100644 --- a/doc/sphinx/addendum/universe-polymorphism.rst +++ b/doc/sphinx/addendum/universe-polymorphism.rst @@ -366,24 +366,32 @@ The syntax has been extended to allow users to explicitly bind names to universes and explicitly instantiate polymorphic definitions. .. cmd:: Universe @ident + Polymorphic Universe @ident In the monorphic case, this command declares a new global universe named :g:`ident`, which can be referred to using its qualified name as well. Global universe names live in a separate namespace. The - command supports the polymorphic flag only in sections, meaning the + command supports the ``Polymorphic`` flag only in sections, meaning the universe quantification will be discharged on each section definition independently. One cannot mix polymorphic and monomorphic declarations in the same section. -.. cmd:: Constraint @ident @ord @ident +.. cmd:: Constraint @universe_constraint + Polymorphic Constraint @universe_constraint - This command declares a new constraint between named universes. The - order relation :n:`@ord` can be one of :math:`<`, :math:`≤` or :math:`=`. If consistent, the constraint - is then enforced in the global environment. Like ``Universe``, it can be - used with the ``Polymorphic`` prefix in sections only to declare - constraints discharged at section closing time. One cannot declare a - global constraint on polymorphic universes. + This command declares a new constraint between named universes. + + .. productionlist:: coq + universe_constraint : `qualid` < `qualid` + : `qualid` <= `qualid` + : `qualid` = `qualid` + + If consistent, the constraint is then enforced in the global + environment. Like :cmd:`Universe`, it can be used with the + ``Polymorphic`` prefix in sections only to declare constraints + discharged at section closing time. One cannot declare a global + constraint on polymorphic universes. .. exn:: Undeclared universe @ident. :undocumented: diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index 701c62cdce..db4ebd5e38 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -656,8 +656,8 @@ changes: attribute. - Removed deprecated commands ``Arguments Scope`` and ``Implicit - Arguments`` in favor of :cmd:`Arguments`, with the help of Jasper - Hugunin. + Arguments`` in favor of :cmd:`Arguments (scopes)` and + :cmd:`Arguments (implicits)`, with the help of Jasper Hugunin. - New flag :flag:`Uniform Inductive Parameters` by Jasper Hugunin to avoid repeating uniform parameters in constructor declarations. diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py index ec3343dac6..53309cd313 100755 --- a/doc/sphinx/conf.py +++ b/doc/sphinx/conf.py @@ -181,7 +181,21 @@ suppress_warnings = ["misc.highlighting_failure"] todo_include_todos = False # Extra warnings, including undefined references -nitpicky = False +nitpicky = True + +nitpick_ignore = [ ('token', token) for token in [ + 'tactic', + # 142 occurrences currently sort of defined in the ltac chapter, + # but is it the right place? + 'module', + 'redexpr', + 'modpath', + 'dirpath', + 'collection', + 'term_pattern', + 'term_pattern_string', + 'command', + 'symbol' ]] # -- Options for HTML output ---------------------------------------------- diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index c48964d66c..c1af4d067f 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -603,11 +603,16 @@ The following experimental command is available when the ``FunInd`` library has The meaning of this declaration is to define a function ident, similarly to ``Fixpoint``. Like in ``Fixpoint``, the decreasing argument must be given (unless the function is not recursive), but it might not - necessarily be *structurally* decreasing. The point of the {} annotation + necessarily be *structurally* decreasing. The point of the :n:`{ @decrease_annot }` annotation is to name the decreasing argument *and* to describe which kind of decreasing criteria must be used to ensure termination of recursive calls. + .. productionlist:: + decrease_annot : struct `ident` + : measure `term` `ident` + : wf `term` `ident` + The ``Function`` construction also enjoys the ``with`` extension to define mutually recursive definitions. However, this feature does not work for non structurally recursive functions. @@ -616,31 +621,33 @@ See the documentation of functional induction (:tacn:`function induction`) and ``Functional Scheme`` (:ref:`functional-scheme`) for how to use the induction principle to easily reason about the function. -Remark: To obtain the right principle, it is better to put rigid -parameters of the function as first arguments. For example it is -better to define plus like this: +.. note:: -.. coqtop:: reset none + To obtain the right principle, it is better to put rigid + parameters of the function as first arguments. For example it is + better to define plus like this: - Require Import FunInd. + .. coqtop:: reset none -.. coqtop:: all + Require Import FunInd. - Function plus (m n : nat) {struct n} : nat := - match n with - | 0 => m - | S p => S (plus m p) - end. + .. coqtop:: all -than like this: + Function plus (m n : nat) {struct n} : nat := + match n with + | 0 => m + | S p => S (plus m p) + end. -.. coqtop:: reset all + than like this: - Function plus (n m : nat) {struct n} : nat := - match n with - | 0 => m - | S p => S (plus p m) - end. + .. coqtop:: reset all + + Function plus (n m : nat) {struct n} : nat := + match n with + | 0 => m + | S p => S (plus p m) + end. *Limitations* @@ -710,7 +717,7 @@ used by ``Function``. A more precise description is given below. with :cmd:`Fixpoint`. Moreover the following are defined: + The same objects as above; - + The fixpoint equation of :token:`ident`: :n:`@ident_equation`. + + The fixpoint equation of :token:`ident`: :token:`ident`\ ``_equation``. .. cmdv:: Function @ident {* @binder } { measure @term @ident } : @type := @term Function @ident {* @binder } { wf @term @ident } : @type := @term @@ -1662,6 +1669,7 @@ Declaring Implicit Arguments of :token:`qualid`. .. cmd:: Arguments @qualid : clear implicits + :name: Arguments (clear implicits) This command clears implicit arguments. @@ -1738,6 +1746,7 @@ Automatic declaration of implicit arguments ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ .. cmd:: Arguments @qualid : default implicits + :name: Arguments (default implicits) This command tells |Coq| to automatically detect what are the implicit arguments of a defined object. @@ -1907,7 +1916,8 @@ This syntax extension is given in the following grammar: Renaming implicit arguments ~~~~~~~~~~~~~~~~~~~~~~~~~~~ -.. cmd:: Arguments @qualid {* @name} : @rename +.. cmd:: Arguments @qualid {* @name} : rename + :name: Arguments (rename) This command is used to redefine the names of implicit arguments. @@ -2293,7 +2303,7 @@ Printing universes language, and can be processed by Graphviz tools. The format is unspecified if `string` doesn’t end in ``.dot`` or ``.gv``. -.. cmdv:: Print Universes Subgraph(@names) +.. cmdv:: Print Universes Subgraph({+ @qualid }) :name: Print Universes Subgraph Prints the graph restricted to the requested names (adjusting diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst index 8acbcbec8f..ebaa6fde66 100644 --- a/doc/sphinx/language/gallina-specification-language.rst +++ b/doc/sphinx/language/gallina-specification-language.rst @@ -185,8 +185,7 @@ is described in Chapter :ref:`syntaxextensionsandinterpretationscopes`. : `qualid` : _ : `num` - : ( `or_pattern` , … , `or_pattern` ) - or_pattern : `pattern` | … | `pattern` + : ( `pattern` | … | `pattern` ) Types diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index fed7111628..c48dd5b99e 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -32,22 +32,25 @@ The syntax of the tactic language is given below. See Chapter :ref:`gallinaspecificationlanguage` for a description of the BNF metasyntax used in these grammar rules. Various already defined entries will be used in this chapter: entries :token:`natural`, :token:`integer`, :token:`ident`, -:token:`qualid`, :token:`term`, :token:`cpattern` and :token:`atomic_tactic` +:token:`qualid`, :token:`term`, :token:`cpattern` and :token:`tactic` represent respectively the natural and integer numbers, the authorized identificators and qualified names, Coq terms and patterns and all the atomic -tactics described in Chapter :ref:`tactics`. The syntax of :token:`cpattern` is +tactics described in Chapter :ref:`tactics`. + +The syntax of :production:`cpattern` is the same as that of terms, but it is extended with pattern matching metavariables. In :token:`cpattern`, a pattern matching metavariable is -represented with the syntax :g:`?id` where :g:`id` is an :token:`ident`. The +represented with the syntax :n:`?@ident`. The notation :g:`_` can also be used to denote metavariable whose instance is -irrelevant. In the notation :g:`?id`, the identifier allows us to keep +irrelevant. In the notation :n:`?@ident`, the identifier allows us to keep instantiations and to make constraints whereas :g:`_` shows that we are not interested in what will be matched. On the right hand side of pattern matching clauses, the named metavariables are used without the question mark prefix. There is also a special notation for second-order pattern matching problems: in an -applicative pattern of the form :g:`@?id id1 … idn`, the variable id matches any -complex expression with (possible) dependencies in the variables :g:`id1 … idn` -and returns a functional term of the form :g:`fun id1 … idn => term`. +applicative pattern of the form :n:`%@?@ident @ident__1 … @ident__n`, +the variable :token:`ident` matches any complex expression with (possible) +dependencies in the variables :n:`@ident__i` and returns a functional term +of the form :n:`fun @ident__1 … ident__n => @term`. The main entry of the grammar is :n:`@expr`. This language is used in proof mode but it can also be used in toplevel definitions as shown below. @@ -121,6 +124,7 @@ mode but it can also be used in toplevel definitions as shown below. : solve [ `expr` | ... | `expr` ] : idtac [ `message_token` ... `message_token`] : fail [`natural`] [`message_token` ... `message_token`] + : gfail [`natural`] [`message_token` ... `message_token`] : fresh [ `component` … `component` ] : context `ident` [`term`] : eval `redexpr` in `term` @@ -132,7 +136,7 @@ mode but it can also be used in toplevel definitions as shown below. : guard `test` : assert_fails `tacexpr3` : assert_succeeds `tacexpr3` - : `atomic_tactic` + : `tactic` : `qualid` `tacarg` ... `tacarg` : `atom` atom : `qualid` @@ -582,11 +586,11 @@ Failing the call to :n:`fail @num` is not enclosed in a :n:`+` command, respecting the algebraic identity. - .. tacv:: fail {* message_token} + .. tacv:: fail {* @message_token} The given tokens are used for printing the failure message. - .. tacv:: fail @num {* message_token} + .. tacv:: fail @num {* @message_token} This is a combination of the previous variants. @@ -597,8 +601,8 @@ Failing Similarly, ``gfail`` fails even when used after ``all:`` and there are no goals left. See the example for clarification. - .. tacv:: gfail {* message_token} - gfail @num {* message_token} + .. tacv:: gfail {* @message_token} + gfail @num {* @message_token} These variants fail with an error message or an error level even if there are no goals left. Be careful however if Coq terms have to be @@ -964,7 +968,7 @@ system decide a name with the intro tactic is not so good since it is very awkward to retrieve the name the system gave. The following expression returns an identifier: -.. tacn:: fresh {* component} +.. tacn:: fresh {* @component} It evaluates to an identifier unbound in the goal. This fresh identifier is obtained by concatenating the value of the :n:`@component`\ s (each of them diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst index aa603fc966..5f2e911ff9 100644 --- a/doc/sphinx/proof-engine/ltac2.rst +++ b/doc/sphinx/proof-engine/ltac2.rst @@ -124,13 +124,13 @@ Type declarations One can define new types by the following commands. -.. cmd:: Ltac2 Type @ltac2_typeparams @lident +.. cmd:: Ltac2 Type {? @ltac2_typeparams } @lident :name: Ltac2 Type This command defines an abstract type. It has no use for the end user and is dedicated to types representing data coming from the OCaml world. -.. cmdv:: Ltac2 Type {? rec} @ltac2_typeparams @lident := @ltac2_typedef +.. cmdv:: Ltac2 Type {? rec} {? @ltac2_typeparams } @lident := @ltac2_typedef This command defines a type with a manifest. There are four possible kinds of such definitions: alias, variant, record and open variant types. @@ -154,7 +154,7 @@ One can define new types by the following commands. Records are product types with named fields and eliminated by projection. Likewise they can be recursive if the `rec` flag is set. - .. cmdv:: Ltac2 Type @ltac2_typeparams @ltac2_qualid := [ @ltac2_constructordef ] + .. cmdv:: Ltac2 Type {? @ltac2_typeparams } @ltac2_qualid ::= [ @ltac2_constructordef ] Open variants are a special kind of variant types whose constructors are not statically defined, but can instead be extended dynamically. A typical example @@ -179,7 +179,7 @@ constructions from ML. : let `ltac2_var` := `ltac2_term` in `ltac2_term` : let rec `ltac2_var` := `ltac2_term` in `ltac2_term` : match `ltac2_term` with `ltac2_branch` ... `ltac2_branch` end - : `int` + : `integer` : `string` : `ltac2_term` ; `ltac2_term` : [| `ltac2_term` ; ... ; `ltac2_term` |] @@ -619,7 +619,7 @@ calls to term matching functions from the `Pattern` module. Internally, it is implemented thanks to a specific scope accepting the :n:`@constrmatching` syntax. Variables from the :n:`@constrpattern` are statically bound in the body of the branch, to -values of type `constr` for the variables from the :n:`@constr` pattern and to a +values of type `constr` for the variables from the :n:`@term` pattern and to a value of type `Pattern.context` for the variable :n:`@lident`. Note that unlike Ltac, only lowercase identifiers are valid as Ltac2 @@ -686,20 +686,22 @@ The following scopes are built-in. - :n:`list0(@ltac2_scope)`: - + if :n:`@ltac2_scope` parses :production:`entry`, parses :n:`(@entry__0, ..., @entry__n)` and produces - :n:`[@entry__0; ...; @entry__n]`. + + if :n:`@ltac2_scope` parses :n:`@quotentry`, + then it parses :n:`(@quotentry__0, ..., @quotentry__n)` and produces + :n:`[@quotentry__0; ...; @quotentry__n]`. - :n:`list0(@ltac2_scope, sep = @string__sep)`: - + if :n:`@ltac2_scope` parses :n:`@entry`, parses :n:`(@entry__0 @string__sep ... @string__sep @entry__n)` - and produces :n:`[@entry__0; ...; @entry__n]`. + + if :n:`@ltac2_scope` parses :n:`@quotentry`, + then it parses :n:`(@quotentry__0 @string__sep ... @string__sep @quotentry__n)` + and produce :n:`[@quotentry__0; ...; @quotentry__n]`. -- :n:`list1`: same as :n:`list0` (with or without separator) but parses :n:`{+ @entry}` instead - of :n:`{* @entry}`. +- :n:`list1`: same as :n:`list0` (with or without separator) but parses :n:`{+ @quotentry}` instead + of :n:`{* @quotentry}`. - :n:`opt(@ltac2_scope)` - + if :n:`@ltac2_scope` parses :n:`@entry`, parses :n:`{? @entry}` and produces either :n:`None` or + + if :n:`@ltac2_scope` parses :n:`@quotentry`, parses :n:`{? @quotentry}` and produces either :n:`None` or :n:`Some x` where :n:`x` is the parsed expression. - :n:`self`: diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst index 4a2f9c0db3..3f966755ca 100644 --- a/doc/sphinx/proof-engine/proof-handling.rst +++ b/doc/sphinx/proof-engine/proof-handling.rst @@ -175,12 +175,12 @@ list of assertion commands is given in :ref:`Assertions`. The command Use all section variables except the list of :token:`ident`. - .. cmdv:: Proof using @collection1 + @collection2 + .. cmdv:: Proof using @collection__1 + @collection__2 Use section variables from the union of both collections. See :ref:`nameaset` to know how to form a named collection. - .. cmdv:: Proof using @collection1 - @collection2 + .. cmdv:: Proof using @collection__1 - @collection__2 Use section variables which are in the first collection but not in the second one. @@ -202,10 +202,10 @@ Proof using options The following options modify the behavior of ``Proof using``. -.. opt:: Default Proof Using "@expression" +.. opt:: Default Proof Using "@collection" :name: Default Proof Using - Use :n:`@expression` as the default ``Proof using`` value. E.g. ``Set Default + Use :n:`@collection` as the default ``Proof using`` value. E.g. ``Set Default Proof Using "a b"`` will complete all ``Proof`` commands not followed by a ``using`` part with ``using a b``. @@ -220,7 +220,7 @@ The following options modify the behavior of ``Proof using``. Name a set of section hypotheses for ``Proof using`` ```````````````````````````````````````````````````` -.. cmd:: Collection @ident := @expression +.. cmd:: Collection @ident := @collection This can be used to name a set of section hypotheses, with the purpose of making ``Proof using`` annotations more diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index b19b0742c1..3149d64d3e 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -1499,7 +1499,7 @@ side of an equation. The abstract tactic ``````````````````` -.. tacn:: abstract: {+ d_item} +.. tacn:: abstract: {+ @d_item} :name: abstract (ssreflect) This tactic assigns an abstract constant previously introduced with the @@ -3478,7 +3478,7 @@ efficient ones, e.g. for the purpose of a correctness proof. Wildcards vs abstractions ````````````````````````` -The rewrite tactic supports :token:`r_items` containing holes. For example, in +The rewrite tactic supports :token:`r_item`\s containing holes. For example, in the tactic ``rewrite (_ : _ * 0 = 0).`` the term ``_ * 0 = 0`` is interpreted as ``forall n : nat, n * 0 = 0.`` Anyway this tactic is *not* equivalent to @@ -3753,7 +3753,7 @@ involves the following steps: 3. If so :tacn:`under` puts these n goals in head normal form (using the defective form of the tactic :tacn:`move`), then executes - the corresponding intro pattern :n:`@ipat__i` in each goal. + the corresponding intro pattern :n:`@i_pattern__i` in each goal. 4. Then :tacn:`under` checks that the first n subgoals are (quantified) equalities or double implications between a @@ -3802,11 +3802,11 @@ One-liner mode The Ltac expression: -:n:`under @term => [ @i_item__1 | … | @i_item__n ] do [ @tac__1 | … | @tac__n ].` +:n:`under @term => [ @i_item__1 | … | @i_item__n ] do [ @tactic__1 | … | @tactic__n ].` can be seen as a shorter form for the following expression: -:n:`(under @term) => [ @i_item__1 | … | @i_item__n | ]; [ @tac__1; over | … | @tac__n; over | cbv beta iota ].` +:n:`(under @term) => [ @i_item__1 | … | @i_item__n | ]; [ @tactic__1; over | … | @tactic__n; over | cbv beta iota ].` Notes: @@ -3819,14 +3819,14 @@ Notes: involving the `bigop` theory from the Mathematical Components library. + If there is only one tactic, the brackets can be omitted, e.g.: - :n:`under @term => i do @tac.` and that shorter form should be + :n:`under @term => i do @tactic.` and that shorter form should be preferred. + If the ``do`` clause is provided and the intro pattern is omitted, then the default :token:`i_item` ``*`` is applied to each branch. E.g., the Ltac expression: - :n:`under @term do [ @tac__1 | … | @tac__n ]` is equivalent to: - :n:`under @term => [ * | … | * ] do [ @tac__1 | … | @tac__n ]` + :n:`under @term do [ @tactic__1 | … | @tactic__n ]` is equivalent to: + :n:`under @term => [ * | … | * ] do [ @tactic__1 | … | @tactic__n ]` (and it can be noted here that the :tacn:`under` tactic performs a ``move.`` before processing the intro patterns ``=> [ * | … | * ]``). @@ -4237,7 +4237,7 @@ selecting a specific redex and has been described in the previous sections. We have seen so far that the possibility of selecting a redex using a term with holes is already a powerful means of redex selection. Similarly, any terms provided by the user in the more -complex forms of :token:`c_patterns` +complex forms of :token:`c_pattern`\s presented in the tables above can contain holes. diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 2ee23df019..67d32835f5 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -462,7 +462,7 @@ Occurrence sets and occurrence clauses An occurrence clause is a modifier to some tactics that obeys the following syntax: - .. productionlist:: sentence + .. productionlist:: coq occurrence_clause : in `goal_occurrences` goal_occurrences : [`ident` [`at_occurrences`], ... , `ident` [`at_occurrences`] [|- [* [`at_occurrences`]]]] : * |- [* [`at_occurrences`]] @@ -2127,7 +2127,7 @@ and an explanation of the underlying technique. :name: discriminate This tactic proves any goal from an assumption stating that two - structurally different :n:`@terms` of an inductive set are equal. For + structurally different :n:`@term`\s of an inductive set are equal. For example, from :g:`(S (S O))=(S O)` we can derive by absurdity any proposition. @@ -2294,7 +2294,7 @@ and an explanation of the underlying technique. .. flag:: Keep Proof Equalities - By default, :tacn:`injection` only creates new equalities between :n:`@terms` + By default, :tacn:`injection` only creates new equalities between :n:`@term`\s whose type is in sort :g:`Type` or :g:`Set`, thus implementing a special behavior for objects that are proofs of a statement in :g:`Prop`. This option controls this behavior. @@ -2703,42 +2703,42 @@ simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`. Uses the equality :n:`@term`:sub:`1` :n:`= @term` :sub:`2` from right to left - .. tacv:: rewrite @term in clause + .. tacv:: rewrite @term in @goal_occurrences - Analogous to :n:`rewrite @term` but rewriting is done following clause - (similarly to :ref:`performing computations <performingcomputations>`). For instance: + Analogous to :n:`rewrite @term` but rewriting is done following + the clause :token:`goal_occurrences`. For instance: - + :n:`rewrite H in H`:sub:`1` will rewrite `H` in the hypothesis - `H`:sub:`1` instead of the current goal. - + :n:`rewrite H in H`:sub:`1` :g:`at 1, H`:sub:`2` :g:`at - 2 |- *` means - :n:`rewrite H; rewrite H in H`:sub:`1` :g:`at 1; rewrite H in H`:sub:`2` :g:`at - 2.` + + :n:`rewrite H in H'` will rewrite `H` in the hypothesis + ``H'`` instead of the current goal. + + :n:`rewrite H in H' at 1, H'' at - 2 |- *` means + :n:`rewrite H; rewrite H in H' at 1; rewrite H in H'' at - 2.` In particular a failure will happen if any of these three simpler tactics fails. - + :n:`rewrite H in * |-` will do :n:`rewrite H in H`:sub:`i` for all hypotheses - :g:`H`:sub:`i` different from :g:`H`. + + :n:`rewrite H in * |-` will do :n:`rewrite H in H'` for all hypotheses + :g:`H'` different from :g:`H`. A success will happen as soon as at least one of these simpler tactics succeeds. + :n:`rewrite H in *` is a combination of :n:`rewrite H` and :n:`rewrite H in * |-` that succeeds if at least one of these two tactics succeeds. Orientation :g:`->` or :g:`<-` can be inserted before the :token:`term` to rewrite. - .. tacv:: rewrite @term at occurrences + .. tacv:: rewrite @term at @occurrences - Rewrite only the given occurrences of :token:`term`. Occurrences are + Rewrite only the given :token:`occurrences` of :token:`term`. Occurrences are specified from left to right as for pattern (:tacn:`pattern`). The rewrite is always performed using setoid rewriting, even for Leibniz’s equality, so one has to ``Import Setoid`` to use this variant. - .. tacv:: rewrite @term by tactic + .. tacv:: rewrite @term by @tactic Use tactic to completely solve the side-conditions arising from the :tacn:`rewrite`. - .. tacv:: rewrite {+, @term} + .. tacv:: rewrite {+, @orientation @term} {? in @ident } Is equivalent to the `n` successive tactics :n:`{+; rewrite @term}`, each one - working on the first subgoal generated by the previous one. Orientation - :g:`->` or :g:`<-` can be inserted before each :token:`term` to rewrite. One + working on the first subgoal generated by the previous one. An :production:`orientation` + ``->`` or ``<-`` can be inserted before each :token:`term` to rewrite. One unique clause can be added at the end after the keyword in; it will then affect all rewrite operations. @@ -2799,13 +2799,14 @@ simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`. Replaces :n:`@term` with :n:`@term’` using the first assumption whose type has the form :n:`@term’ = @term` - .. tacv:: replace @term {? with @term} in clause {? by @tactic} - replace -> @term in clause - replace <- @term in clause + .. tacv:: replace @term {? with @term} in @goal_occurrences {? by @tactic} + replace -> @term in @goal_occurrences + replace <- @term in @goal_occurrences - Acts as before but the replacements take place in the specified clause (see - :ref:`performingcomputations`) and not only in the conclusion of the goal. The - clause argument must not contain any ``type of`` nor ``value of``. + Acts as before but the replacements take place in the specified clauses + (:token:`goal_occurrences`) (see :ref:`performingcomputations`) and not + only in the conclusion of the goal. The clause argument must not contain + any ``type of`` nor ``value of``. .. tacv:: cutrewrite <- (@term = @term’) :name: cutrewrite @@ -2893,7 +2894,7 @@ simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`. This applies :n:`stepl @term` then applies :token:`tactic` to the second goal. - .. tacv:: stepr @term stepr @term by tactic + .. tacv:: stepr @term by @tactic :name: stepr This behaves as :tacn:`stepl` but on the right-hand-side of the binary @@ -3064,7 +3065,7 @@ the conversion in hypotheses :n:`{+ @ident}`. .. tacv:: native_compute :name: native_compute - This tactic evaluates the goal by compilation to Objective Caml as described + This tactic evaluates the goal by compilation to OCaml as described in :cite:`FullReduction`. If Coq is running in native code, it can be typically two to five times faster than ``vm_compute``. Note however that the compilation cost is higher, so it is worth using only for intensive @@ -3159,7 +3160,7 @@ the conversion in hypotheses :n:`{+ @ident}`. + A constant can be marked to be unfolded only if applied to enough arguments. The number of arguments required can be specified using the - ``/`` symbol in the argument list of the :cmd:`Arguments` vernacular command. + ``/`` symbol in the argument list of the :cmd:`Arguments <Arguments (implicits)>` vernacular command. .. example:: @@ -3230,8 +3231,8 @@ the conversion in hypotheses :n:`{+ @ident}`. .. tacv:: simpl @pattern - This applies ``simpl`` only to the subterms matching :n:`@pattern` in the - current goal. + This applies :tacn:`simpl` only to the subterms matching + :n:`@pattern` in the current goal. .. tacv:: simpl @pattern at {+ @num} @@ -3264,50 +3265,77 @@ the conversion in hypotheses :n:`{+ @ident}`. This tactic applies to any goal. The argument qualid must denote a defined transparent constant or local definition (see - :ref:`gallina-definitions` and :ref:`vernac-controlling-the-reduction-strategies`). The tactic - ``unfold`` applies the :math:`\delta` rule to each occurrence of the constant to which - :n:`@qualid` refers in the current goal and then replaces it with its - :math:`\beta`:math:`\iota`-normal form. + :ref:`gallina-definitions` and + :ref:`vernac-controlling-the-reduction-strategies`). The tactic + :tacn:`unfold` applies the :math:`\delta` rule to each occurrence of + the constant to which :n:`@qualid` refers in the current goal and + then replaces it with its :math:`\beta`:math:`\iota`-normal form. -.. exn:: @qualid does not denote an evaluable constant. - :undocumented: + .. exn:: @qualid does not denote an evaluable constant. -.. tacv:: unfold @qualid in @ident + This error is frequent when trying to unfold something that has + defined as an inductive type (or constructor) and not as a + definition. - Replaces :n:`@qualid` in hypothesis :n:`@ident` with its definition - and replaces the hypothesis with its :math:`\beta`:math:`\iota` normal form. + .. example:: -.. tacv:: unfold {+, @qualid} + .. coqtop:: abort all fail - Replaces *simultaneously* :n:`{+, @qualid}` with their definitions and - replaces the current goal with its :math:`\beta`:math:`\iota` normal form. + Goal 0 <= 1. + unfold le. -.. tacv:: unfold {+, @qualid at {+, @num }} + This error can also be raised if you are trying to unfold + something that has been marked as opaque. - The lists :n:`{+, @num}` specify the occurrences of :n:`@qualid` to be - unfolded. Occurrences are located from left to right. + .. example:: - .. exn:: Bad occurrence number of @qualid. - :undocumented: + .. coqtop:: abort all fail - .. exn:: @qualid does not occur. - :undocumented: + Opaque Nat.add. + Goal 1 + 0 = 1. + unfold Nat.add. + + .. tacv:: unfold @qualid in @goal_occurrences -.. tacv:: unfold @string + Replaces :n:`@qualid` in hypothesis (or hypotheses) designated + by :token:`goal_occurrences` with its definition and replaces + the hypothesis with its :math:`\beta`:math:`\iota` normal form. - If :n:`@string` denotes the discriminating symbol of a notation (e.g. "+") or - an expression defining a notation (e.g. `"_ + _"`), and this notation refers to an unfoldable constant, then the - tactic unfolds it. + .. tacv:: unfold {+, @qualid} -.. tacv:: unfold @string%key + Replaces :n:`{+, @qualid}` with their definitions and replaces + the current goal with its :math:`\beta`:math:`\iota` normal + form. - This is variant of :n:`unfold @string` where :n:`@string` gets its - interpretation from the scope bound to the delimiting key :n:`key` - instead of its default interpretation (see :ref:`Localinterpretationrulesfornotations`). -.. tacv:: unfold {+, qualid_or_string at {+, @num}} + .. tacv:: unfold {+, @qualid at @occurrences } - This is the most general form, where :n:`qualid_or_string` is either a - :n:`@qualid` or a :n:`@string` referring to a notation. + The list :token:`occurrences` specify the occurrences of + :n:`@qualid` to be unfolded. Occurrences are located from left + to right. + + .. exn:: Bad occurrence number of @qualid. + :undocumented: + + .. exn:: @qualid does not occur. + :undocumented: + + .. tacv:: unfold @string + + If :n:`@string` denotes the discriminating symbol of a notation + (e.g. "+") or an expression defining a notation (e.g. `"_ + + _"`), and this notation denotes an application whose head symbol + is an unfoldable constant, then the tactic unfolds it. + + .. tacv:: unfold @string%@ident + + This is variant of :n:`unfold @string` where :n:`@string` gets + its interpretation from the scope bound to the delimiting key + :token:`ident` instead of its default interpretation (see + :ref:`Localinterpretationrulesfornotations`). + + .. tacv:: unfold {+, {| @qualid | @string{? %@ident } } {? at @occurrences } } {? in @goal_occurrences } + + This is the most general form. .. tacn:: fold @term :name: fold @@ -3382,14 +3410,13 @@ the conversion in hypotheses :n:`{+ @ident}`. Conversion tactics applied to hypotheses ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -.. tacn:: conv_tactic in {+, @ident} +.. tacn:: @tactic in {+, @ident} - Applies the conversion tactic :n:`conv_tactic` to the hypotheses - :n:`{+ @ident}`. The tactic :n:`conv_tactic` is any of the conversion tactics - listed in this section. + Applies :token:`tactic` (any of the conversion tactics listed in this + section) to the hypotheses :n:`{+ @ident}`. - If :n:`@ident` is a local definition, then :n:`@ident` can be replaced by - (type of :n:`@ident`) to address not the body but the type of the local + If :token:`ident` is a local definition, then :token:`ident` can be replaced by + :n:`type of @ident` to address not the body but the type of the local definition. Example: :n:`unfold not in (type of H1) (type of H3)`. @@ -3447,9 +3474,9 @@ Automation :ref:`The Hints Databases for auto and eauto <thehintsdatabasesforautoandeauto>` for the list of pre-defined databases and the way to create or extend a database. - .. tacv:: auto using {+ @ident__i} {? with {+ @ident } } + .. tacv:: auto using {+ @qualid__i} {? with {+ @ident } } - Uses lemmas :n:`@ident__i` in addition to hints. If :n:`@ident` is an + Uses lemmas :n:`@qualid__i` in addition to hints. If :n:`@qualid` is an inductive type, it is the collection of its constructors which are added as hints. @@ -3457,8 +3484,8 @@ Automation The hints passed through the `using` clause are used in the same way as if they were passed through a hint database. Consequently, - they use a weaker version of :tacn:`apply` and :n:`auto using @ident` - may fail where :n:`apply @ident` succeeds. + they use a weaker version of :tacn:`apply` and :n:`auto using @qualid` + may fail where :n:`apply @qualid` succeeds. Given that this can be seen as counter-intuitive, it could be useful to have an option to use full-blown :tacn:`apply` for lemmas passed @@ -3476,7 +3503,7 @@ Automation Behaves like :tacn:`auto` but shows the tactics it tries to solve the goal, including failing paths. - .. tacv:: {? info_}auto {? @num} {? using {+ @lemma}} {? with {+ @ident}} + .. tacv:: {? info_}auto {? @num} {? using {+ @qualid}} {? with {+ @ident}} This is the most general form, combining the various options. @@ -3489,10 +3516,10 @@ Automation .. tacv:: trivial with {+ @ident} trivial with * - trivial using {+ @lemma} + trivial using {+ @qualid} debug trivial info_trivial - {? info_}trivial {? using {+ @lemma}} {? with {+ @ident}} + {? info_}trivial {? using {+ @qualid}} {? with {+ @ident}} :name: _; _; _; debug trivial; info_trivial; _ :undocumented: @@ -3531,7 +3558,7 @@ Automation Note that ``ex_intro`` should be declared as a hint. - .. tacv:: {? info_}eauto {? @num} {? using {+ @lemma}} {? with {+ @ident}} + .. tacv:: {? info_}eauto {? @num} {? using {+ @qualid}} {? with {+ @ident}} The various options for :tacn:`eauto` are the same as for :tacn:`auto`. @@ -3550,9 +3577,9 @@ Automation This tactic unfolds constants that were declared through a :cmd:`Hint Unfold` in the given databases. -.. tacv:: autounfold with {+ @ident} in clause +.. tacv:: autounfold with {+ @ident} in @goal_occurrences - Performs the unfolding in the given clause. + Performs the unfolding in the given clause (:token:`goal_occurrences`). .. tacv:: autounfold with * @@ -3592,10 +3619,9 @@ Automation Performs all the rewritings in hypothesis :n:`@qualid` applying :n:`@tactic` to the main subgoal after each rewriting step. -.. tacv:: autorewrite with {+ @ident} in @clause +.. tacv:: autorewrite with {+ @ident} in @goal_occurrences - Performs all the rewriting in the clause :n:`@clause`. The clause argument - must not contain any ``type of`` nor ``value of``. + Performs all the rewriting in the clause :n:`@goal_occurrences`. .. seealso:: @@ -3666,10 +3692,11 @@ automatically created. from the order in which they were inserted, making this implementation observationally different from the legacy one. -The general command to add a hint to some databases :n:`{+ @ident}` is - .. cmd:: Hint @hint_definition : {+ @ident} + The general command to add a hint to some databases :n:`{+ @ident}`. + The various possible :production:`hint_definition`\s are given below. + .. cmdv:: Hint @hint_definition No database name is given: the hint is registered in the ``core`` database. @@ -3718,7 +3745,7 @@ The general command to add a hint to some databases :n:`{+ @ident}` is before, the tactic actually used is a restricted version of :tacn:`apply`). - .. cmdv:: Resolve <- @term + .. cmdv:: Hint Resolve <- @term Adds the right-to-left implication of an equivalence as a hint. @@ -3738,7 +3765,7 @@ The general command to add a hint to some databases :n:`{+ @ident}` is .. exn:: @term cannot be used as a hint :undocumented: - .. cmdv:: Immediate {+ @term} : @ident + .. cmdv:: Hint Immediate {+ @term} : @ident Adds each :n:`Hint Immediate @term`. @@ -3981,7 +4008,7 @@ use one or several databases specific to your development. Adds the rewriting rules :n:`{+ @term}` with a right-to-left orientation in the bases :n:`{+ @ident}`. -.. cmd:: Hint Rewrite {+ @term} using tactic : {+ @ident} +.. cmd:: Hint Rewrite {+ @term} using @tactic : {+ @ident} When the rewriting rules :n:`{+ @term}` in :n:`{+ @ident}` will be used, the tactic ``tactic`` will be applied to the generated subgoals, the main subgoal @@ -4202,7 +4229,7 @@ some incompatibilities. Adds lemmas from :tacn:`auto` hint bases :n:`{+ @ident}` to the proof-search environment. -.. tacv:: firstorder tactic using {+ @qualid} with {+ @ident} +.. tacv:: firstorder @tactic using {+ @qualid} with {+ @ident} This combines the effects of the different variants of :tacn:`firstorder`. @@ -4243,10 +4270,10 @@ some incompatibilities. congruence. Qed. -.. tacv:: congruence n +.. tacv:: congruence @num - Tries to add at most `n` instances of hypotheses stating quantified equalities - to the problem in order to solve it. A bigger value of `n` does not make + Tries to add at most :token:`num` instances of hypotheses stating quantified equalities + to the problem in order to solve it. A bigger value of :token:`num` does not make success slower, only failure. You might consider adding some lemmas as hypotheses using assert in order for :tacn:`congruence` to use them. @@ -4556,14 +4583,14 @@ Automating .. _btauto_grammar: .. productionlist:: sentence - t : `x` - : true - : false - : orb `t` `t` - : andb `t` `t` - : xorb `t` `t` - : negb `t` - : if `t` then `t` else `t` + btauto_term : `ident` + : true + : false + : orb `btauto_term` `btauto_term` + : andb `btauto_term` `btauto_term` + : xorb `btauto_term` `btauto_term` + : negb `btauto_term` + : if `btauto_term` then `btauto_term` else `btauto_term` Whenever the formula supplied is not a tautology, it also provides a counter-example. diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index 26dc4e02cf..5f3e82938d 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -189,18 +189,13 @@ Requests to the environment This command displays the type of :n:`@term`. When called in proof mode, the term is checked in the local context of the current subgoal. - - .. TODO : selector is not a syntax entry - .. cmdv:: @selector: Check @term This variant specifies on which subgoal to perform typing (see Section :ref:`invocation-of-tactics`). -.. TODO : convtactic is not a syntax entry - -.. cmd:: Eval @convtactic in @term +.. cmd:: Eval @redexpr in @term This command performs the specified reduction on :n:`@term`, and displays the resulting term with its type. The term to be reduced may depend on @@ -264,11 +259,11 @@ Requests to the environment main symbol as in `"+"` or by its notation’s string as in `"_ + _"` or `"_ 'U' _"`, see Section :ref:`notations`), the command works like ``Search`` :n:`@qualid`. - .. cmdv:: Search @string%@key + .. cmdv:: Search @string%@ident The string string must be a notation or the main symbol of a notation which is then interpreted in the scope bound to - the delimiting key :n:`@key` (see Section :ref:`LocalInterpretationRulesForNotations`). + the delimiting key :token:`ident` (see Section :ref:`LocalInterpretationRulesForNotations`). .. cmdv:: Search @term_pattern @@ -1132,6 +1127,8 @@ described first. with lower level is expanded first. In case of a tie, the second one (appearing in the cast type) is expanded. + .. prodn:: level ::= {| opaque | @num | expand } + Levels can be one of the following (higher to lower): + ``opaque`` : level of opaque constants. They cannot be expanded by @@ -1167,19 +1164,19 @@ described first. Print all the currently non-transparent strategies. -.. cmd:: Declare Reduction @ident := @convtactic +.. cmd:: Declare Reduction @ident := @redexpr This command allows giving a short name to a reduction expression, for - instance lazy beta delta [foo bar]. This short name can then be used + instance ``lazy beta delta [foo bar]``. This short name can then be used in :n:`Eval @ident in` or ``eval`` directives. This command accepts the - Local modifier, for discarding this reduction name at the end of the - file or module. For the moment the name cannot be qualified. In + ``Local`` modifier, for discarding this reduction name at the end of the + file or module. For the moment, the name is not qualified. In particular declaring the same name in several modules or in several - functor applications will be refused if these declarations are not + functor applications will be rejected if these declarations are not local. The name :n:`@ident` cannot be used directly as an Ltac tactic, but - nothing prevents the user to also perform a - :n:`Ltac @ident := @convtactic`. + nothing prevents the user from also performing a + :n:`Ltac @ident := @redexpr`. .. seealso:: :ref:`performingcomputations` @@ -1208,7 +1205,7 @@ Controlling the locality of commands effect of the command to the current module if the command does not occur in a section and the Global modifier extends the effect outside the current sections and current module if the command occurs in a section. As an example, - the :cmd:`Arguments`, :cmd:`Ltac` or :cmd:`Notation` commands belong + the :cmd:`Arguments <Arguments (implicits)>`, :cmd:`Ltac` or :cmd:`Notation` commands belong to this category. Notice that a subclass of these commands do not support extension of their scope outside sections at all and the Global modifier is not applicable to them. diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 6da42f4a48..9b381cb9de 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -109,7 +109,7 @@ the associativity of disjunction and conjunction, so let us apply for instance a right associativity (which is the choice of Coq). Precedence levels and associativity rules of notations have to be -given between parentheses in a list of modifiers that the :cmd:`Notation` +given between parentheses in a list of :token:`modifiers` that the :cmd:`Notation` command understands. Here is how the previous examples refine. .. coqtop:: in @@ -249,7 +249,7 @@ bar of the notation. Check (sig (fun x : nat => x=x)). The second, more powerful control on printing is by using the format -modifier. Here is an example +:token:`modifier`. Here is an example .. coqtop:: all @@ -298,8 +298,8 @@ expression is performed at definition time. Type checking is done only at the time of use of the notation. .. note:: Sometimes, a notation is expected only for the parser. To do - so, the option ``only parsing`` is allowed in the list of modifiers - of :cmd:`Notation`. Conversely, the ``only printing`` modifier can be + so, the option ``only parsing`` is allowed in the list of :token:`modifiers` + of :cmd:`Notation`. Conversely, the ``only printing`` :token:`modifier` can be used to declare that a notation should only be used for printing and should not declare a parsing rule. In particular, such notations do not modify the parser. @@ -310,11 +310,11 @@ The Infix command The :cmd:`Infix` command is a shortening for declaring notations of infix symbols. -.. cmd:: Infix "@symbol" := @term ({+, @modifier}). +.. cmd:: Infix "@symbol" := @term {? (@modifiers) }. This command is equivalent to - :n:`Notation "x @symbol y" := (@term x y) ({+, @modifier}).` + :n:`Notation "x @symbol y" := (@term x y) {? (@modifiers) }.` where ``x`` and ``y`` are fresh names. Here is an example. @@ -437,7 +437,7 @@ application of the notation: Check sigma z : nat, z = 0. -Notice the modifier ``x ident`` in the declaration of the +Notice the :token:`modifier` ``x ident`` in the declaration of the notation. It tells to parse :g:`x` as a single identifier. Binders bound in the notation and parsed as patterns @@ -457,7 +457,7 @@ binder. Here is an example: Check subset '(x,y), x+y=0. -The modifier ``p pattern`` in the declaration of the notation tells to parse +The :token:`modifier` ``p pattern`` in the declaration of the notation tells to parse :g:`p` as a pattern. Note that a single variable is both an identifier and a pattern, so, e.g., the following also works: @@ -467,7 +467,7 @@ pattern, so, e.g., the following also works: If one wants to prevent such a notation to be used for printing when the pattern is reduced to a single identifier, one has to use instead -the modifier ``p strict pattern``. For parsing, however, a +the :token:`modifier` ``p strict pattern``. For parsing, however, a ``strict pattern`` will continue to include the case of a variable. Here is an example showing the difference: @@ -507,7 +507,7 @@ that ``x`` is parsed as a term at level 99 (as done in the notation for :g:`sumbool`), but that this term has actually to be an identifier. The notation :g:`{ x | P }` is already defined in the standard -library with the ``as ident`` modifier. We cannot redefine it but +library with the ``as ident`` :token:`modifier`. We cannot redefine it but one can define an alternative notation, say :g:`{ p such that P }`, using instead ``as pattern``. @@ -527,7 +527,7 @@ is just an identifier, one could have said ``p at level 99 as strict pattern``. Note also that in the absence of a ``as ident``, ``as strict pattern`` or -``as pattern`` modifiers, the default is to consider sub-expressions occurring +``as pattern`` :token:`modifier`\s, the default is to consider sub-expressions occurring in binding position and parsed as terms to be ``as ident``. .. _NotationsWithBinders: @@ -628,7 +628,7 @@ except that in the iterator position of the binding variable of a ``fun`` or a ``forall``. To specify that the part “``x .. y``” of the notation parses a sequence of -binders, ``x`` and ``y`` must be marked as ``binder`` in the list of modifiers +binders, ``x`` and ``y`` must be marked as ``binder`` in the list of :token:`modifiers` of the notation. The binders of the parsed sequence are used to fill the occurrences of the first placeholder of the iterating pattern which is repeatedly nested as many times as the number of binders generated. If ever the @@ -678,7 +678,7 @@ Predefined entries ~~~~~~~~~~~~~~~~~~ By default, sub-expressions are parsed as terms and the corresponding -grammar entry is called :n:`@constr`. However, one may sometimes want +grammar entry is called ``constr``. However, one may sometimes want to restrict the syntax of terms in a notation. For instance, the following notation will accept to parse only global reference in position of :g:`x`: @@ -866,16 +866,17 @@ notations are given below. The optional :production:`scope` is described in :ref:`Scopes`. .. productionlist:: coq - notation : [Local] Notation `string` := `term` [`modifiers`] [: `scope`]. - : [Local] Infix `string` := `qualid` [`modifiers`] [: `scope`]. - : [Local] Reserved Notation `string` [`modifiers`] . + notation : [Local] Notation `string` := `term` [(`modifiers`)] [: `scope`]. + : [Local] Infix `string` := `qualid` [(`modifiers`)] [: `scope`]. + : [Local] Reserved Notation `string` [(`modifiers`)] . : Inductive `ind_body` [`decl_notation`] with … with `ind_body` [`decl_notation`]. : CoInductive `ind_body` [`decl_notation`] with … with `ind_body` [`decl_notation`]. : Fixpoint `fix_body` [`decl_notation`] with … with `fix_body` [`decl_notation`]. : CoFixpoint `cofix_body` [`decl_notation`] with … with `cofix_body` [`decl_notation`]. : [Local] Declare Custom Entry `ident`. decl_notation : [where `string` := `term` [: `scope`] and … and `string` := `term` [: `scope`]]. - modifiers : at level `num` + modifiers : `modifier`, … , `modifier` + modifier : at level `num` : in custom `ident` : in custom `ident` at level `num` : `ident` , … , `ident` at level `num` [`binderinterp`] @@ -924,6 +925,17 @@ notations are given below. The optional :production:`scope` is described in given to some notation, say ``"{ y } & { z }"`` in fact applies to the underlying ``"{ x }"``\-free rule which is ``"y & z"``). +.. note:: Notations such as ``"( p | q )"`` (or starting with ``"( x | "``, + more generally) are deprecated as they conflict with the syntax for + nested disjunctive patterns (see :ref:`extendedpatternmatching`), + and are not honored in pattern expressions. + + .. warn:: Use of @string Notation is deprecated as it is inconsistent with pattern syntax. + + This warning is disabled by default to avoid spurious diagnostics + due to legacy notation in the Coq standard library. + It can be turned on with the ``-w disj-pattern-notation`` flag. + Persistence of notations ++++++++++++++++++++++++ @@ -1032,11 +1044,11 @@ Local opening of an interpretation scope +++++++++++++++++++++++++++++++++++++++++ It is possible to locally extend the interpretation scope stack using the syntax -:g:`(term)%key` (or simply :g:`term%key` for atomic terms), where key is a +:n:`(@term)%@ident` (or simply :n:`@term%@ident` for atomic terms), where :token:`ident` is a special identifier called *delimiting key* and bound to a given scope. In such a situation, the term term, and all its subterms, are -interpreted in the scope stack extended with the scope bound tokey. +interpreted in the scope stack extended with the scope bound to :token:`ident`. .. cmd:: Delimit Scope @scope with @ident @@ -1051,15 +1063,15 @@ interpreted in the scope stack extended with the scope bound tokey. Binding arguments of a constant to an interpretation scope +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ -.. cmd:: Arguments @qualid {+ @name%@scope} +.. cmd:: Arguments @qualid {+ @name%@ident} :name: Arguments (scopes) It is possible to set in advance that some arguments of a given constant have to be interpreted in a given scope. The command is - :n:`Arguments @qualid {+ @name%@scope}` where the list is a prefix of the - arguments of ``qualid`` eventually annotated with their ``scope``. Grouping + :n:`Arguments @qualid {+ @name%@ident}` where the list is a prefix of the + arguments of ``qualid`` optionally annotated with their scope :token:`ident`. Grouping round parentheses can be used to decorate multiple arguments with the same - scope. ``scope`` can be either a scope name or its delimiting key. For + scope. :token:`ident` can be either a scope name or its delimiting key. For example the following command puts the first two arguments of :g:`plus_fct` in the scope delimited by the key ``F`` (``Rfun_scope``) and the last argument in the scope delimited by the key ``R`` (``R_scope``). @@ -1070,13 +1082,13 @@ Binding arguments of a constant to an interpretation scope The ``Arguments`` command accepts scopes decoration to all grouping parentheses. In the following example arguments A and B are marked as - maximally inserted implicit arguments and are put into the type_scope scope. + maximally inserted implicit arguments and are put into the ``type_scope`` scope. .. coqdoc:: Arguments respectful {A B}%type (R R')%signature _ _. - When interpreting a term, if some of the arguments of qualid are built + When interpreting a term, if some of the arguments of :token:`qualid` are built from a notation, then this notation is interpreted in the scope stack extended by the scope bound (if any) to this argument. The effect of the scope is limited to the argument itself. It does not propagate to @@ -1088,21 +1100,21 @@ Binding arguments of a constant to an interpretation scope This command can be used to clear argument scopes of :token:`qualid`. - .. cmdv:: Arguments @qualid {+ @name%scope} : extra scopes + .. cmdv:: Arguments @qualid {+ @name%@ident} : extra scopes Defines extra argument scopes, to be used in case of coercion to ``Funclass`` (see the :ref:`implicitcoercions` chapter) or with a computed type. - .. cmdv:: Global Arguments @qualid {+ @name%@scope} + .. cmdv:: Global Arguments @qualid {+ @name%@ident} - This behaves like :n:`Arguments qualid {+ @name%@scope}` but survives when a + This behaves like :n:`Arguments qualid {+ @name%@ident}` but survives when a section is closed instead of stopping working at section closing. Without the ``Global`` modifier, the effect of the command stops when the section it belongs to ends. - .. cmdv:: Local Arguments @qualid {+ @name%@scope} + .. cmdv:: Local Arguments @qualid {+ @name%@ident} - This behaves like :n:`Arguments @qualid {+ @name%@scope}` but does not + This behaves like :n:`Arguments @qualid {+ @name%@ident}` but does not survive modules and files. Without the ``Local`` modifier, the effect of the command is visible from within other modules or files. @@ -1141,10 +1153,10 @@ Binding types of arguments to an interpretation scope When an interpretation scope is naturally associated to a type (e.g. the scope of operations on the natural numbers), it may be convenient to bind it - to this type. When a scope ``scope`` is bound to a type ``type``, any new function - defined later on gets its arguments of type ``type`` interpreted by default in - scope scope (this default behavior can however be overwritten by explicitly - using the command :cmd:`Arguments`). + to this type. When a scope :token:`scope` is bound to a type :token:`type`, any function + gets its arguments of type :token:`type` interpreted by default in scope :token:`scope` + (this default behavior can however be overwritten by explicitly using the + command :cmd:`Arguments <Arguments (scopes)>`). Whether the argument of a function has some type ``type`` is determined statically. For instance, if ``f`` is a polymorphic function of type @@ -1172,6 +1184,11 @@ Binding types of arguments to an interpretation scope Check (fun x y1 y2 z t => P _ (x + t) ((f _ (y1 + y2) + z))). + .. note:: When active, a bound scope has effect on all defined functions + (even if they are defined after the :cmd:`Bind Scope` directive), except + if argument scopes were assigned explicitly using the + :cmd:`Arguments <Arguments (scopes)>` command. + .. note:: The scopes ``type_scope`` and ``function_scope`` also have a local effect on interpretation. See the next section. @@ -1657,15 +1674,15 @@ Tactic notations allow to customize the syntax of tactics. They have the followi tacn : Tactic Notation [`tactic_level`] [`prod_item` … `prod_item`] := `tactic`. prod_item : `string` | `tactic_argument_type`(`ident`) tactic_level : (at level `num`) - tactic_argument_type : `ident` | `simple_intropattern` | `reference` - : `hyp` | `hyp_list` | `ne_hyp_list` - : `constr` | `uconstr` | `constr_list` | `ne_constr_list` - : `integer` | `integer_list` | `ne_integer_list` - : `int_or_var` | `int_or_var_list` | `ne_int_or_var_list` - : `tactic` | `tactic0` | `tactic1` | `tactic2` | `tactic3` - : `tactic4` | `tactic5` - -.. cmd:: Tactic Notation {? (at level @level)} {+ @prod_item} := @tactic. + tactic_argument_type : ident | simple_intropattern | reference + : hyp | hyp_list | ne_hyp_list + : constr | uconstr | constr_list | ne_constr_list + : integer | integer_list | ne_integer_list + : int_or_var | int_or_var_list | ne_int_or_var_list + : tactic | tactic0 | tactic1 | tactic2 | tactic3 + : tactic4 | tactic5 + +.. cmd:: Tactic Notation {? (at level @num)} {+ @prod_item} := @tactic. A tactic notation extends the parser and pretty-printer of tactics with a new rule made of the list of production items. It then evaluates into the diff --git a/engine/ftactic.ml b/engine/ftactic.ml index dab2e7d5ef..b59d04e813 100644 --- a/engine/ftactic.ml +++ b/engine/ftactic.ml @@ -18,8 +18,8 @@ type 'a focus = (** Type of tactics potentially goal-dependent. If it contains a [Depends], then the length of the inner list is guaranteed to be the number of - currently focussed goals. Otherwise it means the tactic does not depend - on the current set of focussed goals. *) + currently focused goals. Otherwise it means the tactic does not depend + on the current set of focused goals. *) type 'a t = 'a focus Proofview.tactic let return (x : 'a) : 'a t = Proofview.tclUNIT (Uniform x) diff --git a/engine/ftactic.mli b/engine/ftactic.mli index ed95d62bc6..5922781d4d 100644 --- a/engine/ftactic.mli +++ b/engine/ftactic.mli @@ -18,7 +18,7 @@ type +'a t = 'a focus Proofview.tactic (** The type of focussing tactics. A focussing tactic is like a normal tactic, except that it is able to remember it have entered a goal. Whenever this is the case, each subsequent effect of the tactic is dispatched on the - focussed goals. This is a monad. *) + focused goals. This is a monad. *) (** {5 Monadic interface} *) @@ -32,20 +32,20 @@ val bind : 'a t -> ('a -> 'b t) -> 'b t val lift : 'a Proofview.tactic -> 'a t (** Transform a tactic into a focussing tactic. The resulting tactic is not - focussed. *) + focused. *) val run : 'a t -> ('a -> unit Proofview.tactic) -> unit Proofview.tactic (** Given a continuation producing a tactic, evaluates the focussing tactic. If - the tactic has not focussed, then the continuation is evaluated once. - Otherwise it is called in each of the currently focussed goals. *) + the tactic has not focused, then the continuation is evaluated once. + Otherwise it is called in each of the currently focused goals. *) (** {5 Focussing} *) -(** Enter a goal. The resulting tactic is focussed. *) +(** Enter a goal. The resulting tactic is focused. *) val enter : (Proofview.Goal.t -> 'a t) -> 'a t (** Enter a goal, without evar normalization. The resulting tactic is - focussed. *) + focused. *) val with_env : 'a t -> (Environ.env*'a) t (** [with_env t] returns, in addition to the return type of [t], an diff --git a/gramlib/grammar.ml b/gramlib/grammar.ml index c452c7b307..f9d18e7190 100644 --- a/gramlib/grammar.ml +++ b/gramlib/grammar.ml @@ -222,7 +222,7 @@ let is_before : type s1 s2 r1 r2 a1 a2. (s1, r1, a1) ty_symbol -> (s2, r2, a2) t | Stoken _, _ -> true | _ -> false -(** Ancilliary datatypes *) +(** Ancillary datatypes *) type 'a ty_rec = MayRec : ty_mayrec ty_rec | NoRec : ty_norec ty_rec diff --git a/ide/configwin_types.ml b/ide/configwin_types.ml index 251e3dded3..4c66a6944e 100644 --- a/ide/configwin_types.ml +++ b/ide/configwin_types.ml @@ -87,7 +87,7 @@ type modifiers_param = { (** The value, as a list of modifiers and a key code *) md_editable : bool ; (** indicates if the value can be changed *) md_f_apply : Gdk.Tags.modifier list -> unit ; - (** the function to call to apply the new value of the paramter *) + (** the function to call to apply the new value of the parameter *) md_help : string option ; (** optional help string *) md_expand : bool ; (** expand or not *) md_allow : Gdk.Tags.modifier list diff --git a/ide/protocol/interface.ml b/ide/protocol/interface.ml index ccb6bedaf6..9d8fdf6335 100644 --- a/ide/protocol/interface.ml +++ b/ide/protocol/interface.ml @@ -34,7 +34,7 @@ type status = { status_path : string list; (** Module path of the current proof *) status_proofname : string option; - (** Current proof name. [None] if no focussed proof is in progress *) + (** Current proof name. [None] if no focused proof is in progress *) status_allproofs : string list; (** List of all pending proofs. Order is not significant *) status_proofnum : int; @@ -43,7 +43,7 @@ type status = { type 'a pre_goals = { fg_goals : 'a list; - (** List of the focussed goals *) + (** List of the focused goals *) bg_goals : ('a list * 'a list) list; (** Zipper representing the unfocused background goals *) shelved_goals : 'a list; @@ -70,7 +70,7 @@ type option_state = { opt_sync : bool; (** Whether an option is synchronous *) opt_depr : bool; - (** Wheter an option is deprecated *) + (** Whether an option is deprecated *) opt_name : string; (** A short string that is displayed when using [Test] *) opt_value : option_value; diff --git a/ide/protocol/richpp.mli b/ide/protocol/richpp.mli index 31fc7b56f1..18d4b1eeee 100644 --- a/ide/protocol/richpp.mli +++ b/ide/protocol/richpp.mli @@ -25,7 +25,7 @@ type 'annotation located = { of [ppcmds] as a semi-structured document that represents (located) annotations of this string. The [get_annotations] function is used to convert tags into the desired - annotation. [width] sets the printing witdh of the formatter. *) + annotation. [width] sets the printing width of the formatter. *) val rich_pp : int -> Pp.t -> Pp.pp_tag located Xml_datatype.gxml (** [annotations_positions ssdoc] returns a list associating each diff --git a/ide/protocol/xml_printer.mli b/ide/protocol/xml_printer.mli index 178f7c808f..4b47aa9f7c 100644 --- a/ide/protocol/xml_printer.mli +++ b/ide/protocol/xml_printer.mli @@ -16,11 +16,11 @@ type target = TChannel of out_channel | TBuffer of Buffer.t val make : target -> t (** Print the xml data structure to a source into a compact xml string (without - any user-readable formating ). *) + any user-readable formatting ). *) val print : t -> xml -> unit (** Print the xml data structure into a compact xml string (without - any user-readable formating ). *) + any user-readable formatting ). *) val to_string : xml -> string (** Print the xml data structure into an user-readable string with diff --git a/ide/protocol/xmlprotocol.ml b/ide/protocol/xmlprotocol.ml index e18219210f..5b37ca35ed 100644 --- a/ide/protocol/xmlprotocol.ml +++ b/ide/protocol/xmlprotocol.ml @@ -405,7 +405,7 @@ end = struct | (lg, rg) :: l -> Printf.sprintf "%i:%a" (List.length lg + List.length rg) pr_focus l in - Printf.sprintf "Still focussed: [%a]." pr_focus g.bg_goals + Printf.sprintf "Still focused: [%a]." pr_focus g.bg_goals else let pr_goal { goal_hyp = hyps; goal_ccl = goal } = "[" ^ String.concat "; " (List.map Pp.string_of_ppcmds hyps) ^ " |- " ^ diff --git a/interp/constrextern.ml b/interp/constrextern.ml index bb66658a37..fe50bd4b08 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -107,7 +107,7 @@ let _show_inactive_notations () = let deactivate_notation nr = match nr with | SynDefRule kn -> - (* shouldn't we check wether it is well defined? *) + (* shouldn't we check whether it is well defined? *) inactive_notations_table := IRuleSet.add nr !inactive_notations_table | NotationRule (scopt, ntn) -> match availability_of_notation (scopt, ntn) (scopt, []) with diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 753065b7dd..1dd68f2abf 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1229,7 +1229,7 @@ let add_local_defs_and_check_length loc env g pl args = match g with let maxargs = Inductiveops.constructor_nalldecls env cstr in if List.length pl' + List.length args > maxargs then error_wrong_numarg_constructor ?loc env cstr (Inductiveops.constructor_nrealargs env cstr); - (* Two possibilities: either the args are given with explict + (* Two possibilities: either the args are given with explicit variables for local definitions, then we give the explicit args extended with local defs, so that there is nothing more to be added later on; or the args are not enough to have all arguments, @@ -1467,7 +1467,7 @@ let alias_of als = match als.alias_ids with @returns a raw_case_pattern_expr : - no notations and syntactic definition - - global reference and identifeir instead of reference + - global reference and identifier instead of reference *) @@ -1642,15 +1642,13 @@ let drop_notations_pattern looked_for genv = | CPatCast (_,_) -> (* We raise an error if the pattern contains a cast, due to current restrictions on casts in patterns. Cast in patterns - are supportted only in local binders and only at top - level. In fact, they are currently eliminated by the - parser. The only reason why they are in the - [cases_pattern_expr] type is that the parser needs to factor - the "(c : t)" notation with user defined notations (such as - the pair). In the long term, we will try to support such - casts everywhere, and use them to print the domains of - lambdas in the encoding of match in constr. This check is - here and not in the parser because it would require + are supported only in local binders and only at top level. + The only reason they are in the [cases_pattern_expr] type + is that the parser needs to factor the "c : t" notation + with user defined notations. In the long term, we will try to + support such casts everywhere, and perhaps use them to print + the domains of lambdas in the encoding of match in constr. + This check is here and not in the parser because it would require duplicating the levels of the [pattern] rule. *) CErrors.user_err ?loc ~hdr:"drop_notations_pattern" (Pp.strbrk "Casts are not supported in this pattern.") diff --git a/interp/declare.mli b/interp/declare.mli index 2ffde31fc0..795d9a767d 100644 --- a/interp/declare.mli +++ b/interp/declare.mli @@ -40,7 +40,7 @@ type internal_flag = | InternalTacticRequest | UserIndividualRequest -(* Defaut definition entries, transparent with no secctx or proj information *) +(* Default definition entries, transparent with no secctx or proj information *) val definition_entry : ?fix_exn:Future.fix_exn -> ?opaque:bool -> ?inline:bool -> ?types:types -> ?univs:Entries.universes_entry -> diff --git a/interp/impargs.ml b/interp/impargs.ml index 806fe93297..f3cdd64633 100644 --- a/interp/impargs.ml +++ b/interp/impargs.ml @@ -96,11 +96,11 @@ let set_maximality imps b = this kind if there is enough arguments to infer them) - [DepFlex] means that the implicit argument can be found by unification - along a collapsable path only (e.g. as x in (P x) where P is another + along a collapsible path only (e.g. as x in (P x) where P is another argument) (we do (defensively) print the arguments of this kind) - [DepFlexAndRigid] means that the least argument from which the - implicit argument can be inferred is following a collapsable path + implicit argument can be inferred is following a collapsible path but there is a greater argument from where the implicit argument is inferable following a rigid path (useful to know how to print a partial application) diff --git a/interp/impargs.mli b/interp/impargs.mli index ccdd448460..1099074c63 100644 --- a/interp/impargs.mli +++ b/interp/impargs.mli @@ -34,7 +34,7 @@ val with_implicit_protection : ('a -> 'b) -> 'a -> 'b (** {6 ... } *) (** An [implicits_list] is a list of positions telling which arguments - of a reference can be automatically infered *) + of a reference can be automatically inferred *) type argument_position = @@ -50,11 +50,11 @@ type implicit_explanation = this kind if there is enough arguments to infer them) *) | DepFlex of argument_position (** means that the implicit argument can be found by unification - along a collapsable path only (e.g. as x in (P x) where P is another + along a collapsible path only (e.g. as x in (P x) where P is another argument) (we do (defensively) print the arguments of this kind) *) | DepFlexAndRigid of (*flex*) argument_position * (*rig*) argument_position (** means that the least argument from which the - implicit argument can be inferred is following a collapsable path + implicit argument can be inferred is following a collapsible path but there is a greater argument from where the implicit argument is inferable following a rigid path (useful to know how to print a partial application) *) diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml index 49273c4146..a7e1de736c 100644 --- a/interp/syntax_def.ml +++ b/interp/syntax_def.ml @@ -48,7 +48,7 @@ let open_syntax_constant i ((sp,kn),(_,pat,onlyparse)) = match onlyparse with | None -> (* Redeclare it to be used as (short) name in case an other (distfix) - notation was declared inbetween *) + notation was declared in between *) Notation.declare_uninterpretation (Notation.SynDefRule kn) pat | _ -> () end diff --git a/kernel/byterun/coq_memory.c b/kernel/byterun/coq_memory.c index 542a05fd25..a1c49bee95 100644 --- a/kernel/byterun/coq_memory.c +++ b/kernel/byterun/coq_memory.c @@ -105,7 +105,7 @@ value init_coq_vm(value unit) /* ML */ init_coq_interpreter(); /* Some predefined pointer code. - * It is typically contained in accumlator blocks whose tag is 0 and thus + * It is typically contained in accumulator blocks whose tag is 0 and thus * scanned by the GC, so make it look like an OCaml block. */ value accu_block = (value) coq_stat_alloc(2 * sizeof(value)); Hd_hp (accu_block) = Make_header (1, Abstract_tag, Caml_black); \ diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml index 95f88c0306..fc7d1a54f2 100644 --- a/kernel/cClosure.ml +++ b/kernel/cClosure.ml @@ -226,7 +226,7 @@ let unfold_red kn = * this constant or abstraction. * * i_tab is the cache table of the results * - * ref_value_cache searchs in the tab, otherwise uses i_repr to + * ref_value_cache searches in the tab, otherwise uses i_repr to * compute the result and store it in the table. If the constant can't * be unfolded, returns None, but does not store this failure. * This * doesn't take the RESET into account. You mustn't keep such a table @@ -645,7 +645,7 @@ and subst_constr subst c = match [@ocaml.warning "-4"] Constr.kind c with and comp_subs el s = Esubst.lift_subst (fun el c -> lazy (to_constr el c)) el s -(* This function defines the correspondance between constr and +(* This function defines the correspondence between constr and fconstr. When we find a closure whose substitution is the identity, then we directly return the constr to avoid possibly huge reallocation. *) diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli index 1a790eaed6..60185464c5 100644 --- a/kernel/cClosure.mli +++ b/kernel/cClosure.mli @@ -200,7 +200,7 @@ val whd_val : clos_infos -> clos_tab -> fconstr -> constr val whd_stack : clos_infos -> clos_tab -> fconstr -> stack -> fconstr * stack -(** [eta_expand_ind_stack env ind c s t] computes stacks correspoding +(** [eta_expand_ind_stack env ind c s t] computes stacks corresponding to the conversion of the eta expansion of t, considered as an inhabitant of ind, and the Constructor c of this inductive type applied to arguments s. diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml index 69f004307d..90fbcb8ae3 100644 --- a/kernel/cbytegen.ml +++ b/kernel/cbytegen.ml @@ -386,7 +386,7 @@ let rec is_tailcall = function | Klabel _ :: c -> is_tailcall c | _ -> None -(* Extention of the continuation *) +(* Extension of the continuation *) (* Add a Kpop n instruction in front of a continuation *) let rec add_pop n = function diff --git a/kernel/constr.mli b/kernel/constr.mli index 7fc57cdb8a..aa5878c9d7 100644 --- a/kernel/constr.mli +++ b/kernel/constr.mli @@ -141,7 +141,7 @@ val mkRef : GlobRef.t Univ.puniverses -> constr [mkCase ci p c ac] stand for match [c] as [x] in [I args] return [p] with [ac] presented as describe in [ci]. - [p] stucture is [fun args x -> "return clause"] + [p] structure is [fun args x -> "return clause"] [ac]{^ ith} element is ith constructor case presented as {e lambda construct_args (without params). case_term } *) diff --git a/kernel/declarations.ml b/kernel/declarations.ml index 36ee952099..860d19fe26 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -22,11 +22,11 @@ type engagement = set_predicativity (** {6 Representation of constants (Definition/Axiom) } *) (** Non-universe polymorphic mode polymorphism (Coq 8.2+): inductives - and constants hiding inductives are implicitely polymorphic when + and constants hiding inductives are implicitly polymorphic when applied to parameters, on the universes appearing in the whnf of their parameters and their conclusion, in a template style. - In truely universe polymorphic mode, we always use RegularArity. + In truly universe polymorphic mode, we always use RegularArity. *) type template_arity = { diff --git a/kernel/inductive.ml b/kernel/inductive.ml index d9335d39b5..ca7086a3e4 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -166,7 +166,7 @@ let make_subst env = (* template, it is identity substitution otherwise (ie. when u is *) (* already in the domain of the substitution) [remember_subst] will *) (* update its image [x] by [sup x u] in order not to forget the *) - (* dependency in [u] that remains to be fullfilled. *) + (* dependency in [u] that remains to be fulfilled. *) make (remember_subst u subst) (sign, exp, []) | _sign, [], _ -> (* Uniform parameters are exhausted *) diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index 2de5faa6df..72393d0081 100644 --- a/kernel/mod_typing.ml +++ b/kernel/mod_typing.ml @@ -188,7 +188,7 @@ let rec check_with_mod env struc (idl,mp1) mp equiv = in let new_equiv = add_delta_resolver equiv new_mb.mod_delta in (* we propagate the new equality in the rest of the signature - with the identity substitution accompagned by the new resolver*) + with the identity substitution accompanied by the new resolver*) let id_subst = map_mp mp' mp' new_mb.mod_delta in let new_after = subst_structure id_subst after in before@(lab,SFBmodule new_mb')::new_after, new_equiv, cst diff --git a/kernel/modops.ml b/kernel/modops.ml index 4fdd7ab334..472fddb829 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -515,7 +515,7 @@ and strengthen_and_subst_struct str subst mp_from mp_to alias incl reso = "Module M:=P." or "Module M. Include P. End M." We need to perform two operations to compute the body of M. - The first one is applying the substitution {P <- M} on the type of P - - The second one is strenghtening. *) + - The second one is strengthening. *) let strengthen_and_subst_mb mb mp include_b = match mb.mod_type with |NoFunctor struc -> diff --git a/kernel/uint63.mli b/kernel/uint63.mli index f25f24512d..93632da110 100644 --- a/kernel/uint63.mli +++ b/kernel/uint63.mli @@ -13,7 +13,7 @@ val of_uint : int -> t val hash : t -> int - (* convertion to a string *) + (* conversion to a string *) val to_string : t -> string val of_string : string -> t diff --git a/kernel/univ.ml b/kernel/univ.ml index b1bbc25fe6..2b88d6884d 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -726,7 +726,7 @@ let univ_level_rem u v min = | Some u' -> if Level.equal u u' then min else v | None -> List.filter (fun (l, n) -> not (Int.equal n 0 && Level.equal u l)) v -(* Is u mentionned in v (or equals to v) ? *) +(* Is u mentioned in v (or equals to v) ? *) (**********************************************************************) diff --git a/kernel/univ.mli b/kernel/univ.mli index db178c4bb0..ddb204dd52 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -163,7 +163,7 @@ val super : Universe.t -> Universe.t val universe_level : Universe.t -> Level.t option -(** [univ_level_mem l u] Is l is mentionned in u ? *) +(** [univ_level_mem l u] Is l is mentioned in u ? *) val univ_level_mem : Level.t -> Universe.t -> bool diff --git a/kernel/vmvalues.ml b/kernel/vmvalues.ml index 777a207013..5e3a3c3347 100644 --- a/kernel/vmvalues.ml +++ b/kernel/vmvalues.ml @@ -12,7 +12,7 @@ open Univ open Constr (*******************************************) -(* Initalization of the abstract machine ***) +(* Initialization of the abstract machine ***) (* Necessary for [relaccu_tbl] *) (*******************************************) diff --git a/lib/cProfile.mli b/lib/cProfile.mli index 764faf8d1a..00babe1a47 100644 --- a/lib/cProfile.mli +++ b/lib/cProfile.mli @@ -18,7 +18,7 @@ To trace a function "f" you first need to get a key for it by using : let fkey = declare_profile "f";; -(the string is used to print the profile infomation). Warning: this +(the string is used to print the profile information). Warning: this function does a side effect. Choose the ident you want instead "fkey". Then if the function has ONE argument add the following just after diff --git a/lib/envars.mli b/lib/envars.mli index ebf86d0650..558fe74042 100644 --- a/lib/envars.mli +++ b/lib/envars.mli @@ -38,7 +38,7 @@ val datadir : unit -> string (** [configdir] is the path to the installed config directory. *) val configdir : unit -> string -(** [set_coqlib] must be runned once before any access to [coqlib] *) +(** [set_coqlib] must be run once before any access to [coqlib] *) val set_coqlib : fail:(string -> string) -> unit (** [set_user_coqlib path] sets the coqlib directory explicitedly. *) diff --git a/lib/feedback.mli b/lib/feedback.mli index f407e2fd5b..c9e6ca1266 100644 --- a/lib/feedback.mli +++ b/lib/feedback.mli @@ -56,7 +56,7 @@ type feedback = { (** {6 Feedback sent, even asynchronously, to the user interface} *) -(* The interpreter assignes an state_id to the ast, and feedbacks happening +(* The interpreter assigns a state_id to the ast, and feedbacks happening * during interpretation are attached to it. *) diff --git a/lib/flags.mli b/lib/flags.mli index a70a23b902..535b46950e 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -64,7 +64,7 @@ val beautify : bool ref val beautify_file : bool ref (* Coq quiet mode. Note that normal mode is called "verbose" here, - whereas [quiet] supresses normal output such as goals in coqtop *) + whereas [quiet] suppresses normal output such as goals in coqtop *) val quiet : bool ref val silently : ('a -> 'b) -> 'a -> 'b val verbosely : ('a -> 'b) -> 'a -> 'b diff --git a/lib/pp.mli b/lib/pp.mli index 4ce6a535c8..8b3a07d4b2 100644 --- a/lib/pp.mli +++ b/lib/pp.mli @@ -18,7 +18,7 @@ (* to interpret. *) (* *) (* The datatype has a public view to allow serialization or advanced *) -(* uses, however regular users are _strongly_ warned againt its use, *) +(* uses, however regular users are _strongly_ warned against its use, *) (* they should instead rely on the available functions below. *) (* *) (* Box order and number is indeed an important factor. Try to create *) diff --git a/lib/pp_diff.mli b/lib/pp_diff.mli index 03468271d2..0eec18bd5a 100644 --- a/lib/pp_diff.mli +++ b/lib/pp_diff.mli @@ -88,7 +88,7 @@ Ppcmd_strings will be split into multiple Ppcmd_strings if a diff starts or ends in the middle of the string. Whitespace just before or just after a diff will not be part of the highlight. -Prexisting tags in pp may contain only a single Ppcmd_string. Those tags will be +Preexisting tags in pp may contain only a single Ppcmd_string. Those tags will be placed inside the diff tags to ensure proper nesting of tags within spans of "start.diff.*" ... "end.diff.*". diff --git a/lib/spawn.mli b/lib/spawn.mli index 944aa27a7f..24bbded4f1 100644 --- a/lib/spawn.mli +++ b/lib/spawn.mli @@ -9,7 +9,7 @@ (************************************************************************) (* This module implements spawning/killing managed processes with a - * synchronous or asynchronous comunication channel that works with + * synchronous or asynchronous communication channel that works with * threads or with a glib like main loop model. * * This module requires no threads and no main loop model. It takes care diff --git a/library/declaremods.ml b/library/declaremods.ml index 5fd11e187a..d74bdd484c 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -51,7 +51,7 @@ let inl2intopt = function - Then comes either the object segment itself (for interactive modules), or a compact way to store derived objects (path to - a earlier module + subtitution). + a earlier module + substitution). *) type algebraic_objects = diff --git a/library/library.ml b/library/library.ml index 500e77f89b..9f4eb531ed 100644 --- a/library/library.ml +++ b/library/library.ml @@ -208,7 +208,7 @@ let register_open_library export m = let open_library export explicit_libs m = if (* Only libraries indirectly to open are not reopen *) - (* Libraries explicitly mentionned by the user are always reopen *) + (* Libraries explicitly mentioned by the user are always reopen *) List.exists (fun m' -> DirPath.equal m m') explicit_libs || not (library_is_opened m) then begin @@ -264,90 +264,11 @@ let in_import_library : DirPath.t list * bool -> obj = subst_function = subst_import_library; classify_function = classify_import_library } - -(************************************************************************) -(*s Locate absolute or partially qualified library names in the path *) - -exception LibUnmappedDir -exception LibNotFound -type library_location = LibLoaded | LibInPath - -let warn_several_object_files = - CWarnings.create ~name:"several-object-files" ~category:"require" - (fun (vi, vo) -> str"Loading" ++ spc () ++ str vi ++ - strbrk " instead of " ++ str vo ++ - strbrk " because it is more recent") - -let locate_absolute_library dir = - (* Search in loadpath *) - let pref, base = split_dirpath dir in - let loadpath = Loadpath.filter_path (fun dir -> DirPath.equal dir pref) in - let () = match loadpath with [] -> raise LibUnmappedDir | _ -> () in - let loadpath = List.map fst loadpath in - let find ext = - try - let name = Id.to_string base ^ ext in - let _, file = System.where_in_path ~warn:false loadpath name in - Some file - with Not_found -> None in - match find ".vo", find ".vio" with - | None, None -> raise LibNotFound - | Some file, None | None, Some file -> file - | Some vo, Some vi when Unix.((stat vo).st_mtime < (stat vi).st_mtime) -> - warn_several_object_files (vi, vo); - vi - | Some vo, Some _ -> vo - -let locate_qualified_library ?root ?(warn = true) qid = - (* Search library in loadpath *) - let dir, base = repr_qualid qid in - let loadpath = Loadpath.expand_path ?root dir in - let () = match loadpath with [] -> raise LibUnmappedDir | _ -> () in - let find ext = - try - let name = Id.to_string base ^ ext in - let lpath, file = - System.where_in_path ~warn (List.map fst loadpath) name in - Some (lpath, file) - with Not_found -> None in - let lpath, file = - match find ".vo", find ".vio" with - | None, None -> raise LibNotFound - | Some res, None | None, Some res -> res - | Some (_, vo), Some (_, vi as resvi) - when Unix.((stat vo).st_mtime < (stat vi).st_mtime) -> - warn_several_object_files (vi, vo); - resvi - | Some resvo, Some _ -> resvo - in - let dir = add_dirpath_suffix (String.List.assoc lpath loadpath) base in - (* Look if loaded *) - if library_is_loaded dir then (LibLoaded, dir,library_full_filename dir) - (* Otherwise, look for it in the file system *) - else (LibInPath, dir, file) - -let error_unmapped_dir qid = - let prefix, _ = repr_qualid qid in - user_err ~hdr:"load_absolute_library_from" - (str "Cannot load " ++ pr_qualid qid ++ str ":" ++ spc () ++ - str "no physical path bound to" ++ spc () ++ DirPath.print prefix ++ fnl ()) - -let error_lib_not_found qid = - user_err ~hdr:"load_absolute_library_from" - (str"Cannot find library " ++ pr_qualid qid ++ str" in loadpath") - -let try_locate_absolute_library dir = - try - locate_absolute_library dir - with - | LibUnmappedDir -> error_unmapped_dir (qualid_of_dirpath dir) - | LibNotFound -> error_lib_not_found (qualid_of_dirpath dir) - (************************************************************************) (** {6 Tables of opaque proof terms} *) (** We now store opaque proof terms apart from the rest of the environment. - See the [Indirect] contructor in [Lazyconstr.lazy_constr]. This way, + See the [Indirect] constructor in [Lazyconstr.lazy_constr]. This way, we can quickly load a first half of a .vo file without these opaque terms, and access them only when a specific command (e.g. Print or Print Assumptions) needs it. *) @@ -450,7 +371,7 @@ let intern_from_file f = module DPMap = Map.Make(DirPath) -let rec intern_library (needed, contents) (dir, f) from = +let rec intern_library ~lib_resolver (needed, contents) (dir, f) from = (* Look if in the current logical environment *) try (find_library dir).libsum_digests, (needed, contents) with Not_found -> @@ -459,7 +380,7 @@ let rec intern_library (needed, contents) (dir, f) from = with Not_found -> Feedback.feedback(Feedback.FileDependency (from, DirPath.to_string dir)); (* [dir] is an absolute name which matches [f] which must be in loadpath *) - let f = match f with Some f -> f | None -> try_locate_absolute_library dir in + let f = match f with Some f -> f | None -> lib_resolver dir in let m = intern_from_file f in if not (DirPath.equal dir m.library_name) then user_err ~hdr:"load_physical_library" @@ -467,22 +388,24 @@ let rec intern_library (needed, contents) (dir, f) from = DirPath.print m.library_name ++ spc () ++ str "and not library" ++ spc() ++ DirPath.print dir); Feedback.feedback (Feedback.FileLoaded(DirPath.to_string dir, f)); - m.library_digests, intern_library_deps (needed, contents) dir m f + m.library_digests, intern_library_deps ~lib_resolver (needed, contents) dir m f -and intern_library_deps libs dir m from = - let needed, contents = Array.fold_left (intern_mandatory_library dir from) libs m.library_deps in +and intern_library_deps ~lib_resolver libs dir m from = + let needed, contents = + Array.fold_left (intern_mandatory_library ~lib_resolver dir from) + libs m.library_deps in (dir :: needed, DPMap.add dir m contents ) -and intern_mandatory_library caller from libs (dir,d) = - let digest, libs = intern_library libs (dir, None) (Some from) in +and intern_mandatory_library ~lib_resolver caller from libs (dir,d) = + let digest, libs = intern_library ~lib_resolver libs (dir, None) (Some from) in if not (Safe_typing.digest_match ~actual:digest ~required:d) then user_err (str "Compiled library " ++ DirPath.print caller ++ str " (in file " ++ str from ++ str ") makes inconsistent assumptions \ over library " ++ DirPath.print dir); libs -let rec_intern_library libs (dir, f) = - let _, libs = intern_library libs (dir, Some f) None in +let rec_intern_library ~lib_resolver libs (dir, f) = + let _, libs = intern_library ~lib_resolver libs (dir, Some f) None in libs let native_name_from_filename f = @@ -557,8 +480,8 @@ let warn_require_in_module = strbrk "You can Require a module at toplevel " ++ strbrk "and optionally Import it inside another one.") -let require_library_from_dirpath modrefl export = - let needed, contents = List.fold_left rec_intern_library ([], DPMap.empty) modrefl in +let require_library_from_dirpath ~lib_resolver modrefl export = + let needed, contents = List.fold_left (rec_intern_library ~lib_resolver) ([], DPMap.empty) modrefl in let needed = List.rev_map (fun dir -> DPMap.find dir contents) needed in let modrefl = List.map fst modrefl in if Lib.is_module_or_modtype () then diff --git a/library/library.mli b/library/library.mli index 390299bf56..f3186d847f 100644 --- a/library/library.mli +++ b/library/library.mli @@ -22,7 +22,11 @@ open Libnames (** {6 ... } Require = load in the environment + open (if the optional boolean is not [None]); mark also for export if the boolean is [Some true] *) -val require_library_from_dirpath : (DirPath.t * string) list -> bool option -> unit +val require_library_from_dirpath + : lib_resolver:(DirPath.t -> CUnix.physical_path) + -> (DirPath.t * string) list + -> bool option + -> unit (** {6 Start the compilation of a library } *) @@ -45,8 +49,10 @@ val save_library_to : output_native_objects:bool -> DirPath.t -> string -> Opaqueproof.opaquetab -> unit -val load_library_todo : - string -> seg_sum * seg_lib * seg_univ * seg_discharge * 'tasks * seg_proofs +val load_library_todo + : CUnix.physical_path + -> seg_sum * seg_lib * seg_univ * seg_discharge * 'tasks * seg_proofs + val save_library_raw : string -> seg_sum -> seg_lib -> seg_univ -> seg_proofs -> unit (** {6 Interrogate the status of libraries } *) @@ -65,20 +71,5 @@ val library_full_filename : DirPath.t -> string (** - Overwrite the filename of all libraries (used when restoring a state) *) val overwrite_library_filenames : string -> unit -(** {6 Locate a library in the load paths } *) -exception LibUnmappedDir -exception LibNotFound -type library_location = LibLoaded | LibInPath - -val locate_qualified_library : - ?root:DirPath.t -> ?warn:bool -> qualid -> - library_location * DirPath.t * CUnix.physical_path -(** Locates a library by implicit name. - - @raise LibUnmappedDir if the library is not in the path - @raise LibNotFound if there is no corresponding file in the path - -*) - (** {6 Native compiler. } *) val native_name_from_filename : string -> string diff --git a/library/library.mllib b/library/library.mllib index 8f694f4a31..ef53471377 100644 --- a/library/library.mllib +++ b/library/library.mllib @@ -7,7 +7,6 @@ Global Decl_kinds Lib Declaremods -Loadpath Library States Kindops diff --git a/library/loadpath.ml b/library/loadpath.ml deleted file mode 100644 index fc13c864d0..0000000000 --- a/library/loadpath.ml +++ /dev/null @@ -1,119 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -open Pp -open Util -open CErrors -open Names -open Libnames - -(** Load paths. Mapping from physical to logical paths. *) - -type t = { - path_physical : CUnix.physical_path; - path_logical : DirPath.t; - path_implicit : bool; -} - -let load_paths = Summary.ref ([] : t list) ~name:"LOADPATHS" - -let logical p = p.path_logical - -let physical p = p.path_physical - -let get_load_paths () = !load_paths - -let anomaly_too_many_paths path = - anomaly (str "Several logical paths are associated to" ++ spc () ++ str path ++ str ".") - -let find_load_path phys_dir = - let phys_dir = CUnix.canonical_path_name phys_dir in - let filter p = String.equal p.path_physical phys_dir in - let paths = List.filter filter !load_paths in - match paths with - | [] -> raise Not_found - | [p] -> p - | _ -> anomaly_too_many_paths phys_dir - -let is_in_load_paths phys_dir = - let dir = CUnix.canonical_path_name phys_dir in - let lp = get_load_paths () in - let check_p p = String.equal dir p.path_physical in - List.exists check_p lp - -let remove_load_path dir = - let filter p = not (String.equal p.path_physical dir) in - load_paths := List.filter filter !load_paths - -let warn_overriding_logical_loadpath = - CWarnings.create ~name:"overriding-logical-loadpath" ~category:"loadpath" - (fun (phys_path, old_path, coq_path) -> - str phys_path ++ strbrk " was previously bound to " ++ - DirPath.print old_path ++ strbrk "; it is remapped to " ++ - DirPath.print coq_path) - -let add_load_path phys_path coq_path ~implicit = - let phys_path = CUnix.canonical_path_name phys_path in - let filter p = String.equal p.path_physical phys_path in - let binding = { - path_logical = coq_path; - path_physical = phys_path; - path_implicit = implicit; - } in - match List.filter filter !load_paths with - | [] -> - load_paths := binding :: !load_paths - | [{ path_logical = old_path; path_implicit = old_implicit }] -> - let replace = - if DirPath.equal coq_path old_path then - implicit <> old_implicit - else - let () = - (* Do not warn when overriding the default "-I ." path *) - if not (DirPath.equal old_path Libnames.default_root_prefix) then - warn_overriding_logical_loadpath (phys_path, old_path, coq_path) - in - true in - if replace then - begin - remove_load_path phys_path; - load_paths := binding :: !load_paths; - end - | _ -> anomaly_too_many_paths phys_path - -let filter_path f = - let rec aux = function - | [] -> [] - | p :: l -> - if f p.path_logical then (p.path_physical, p.path_logical) :: aux l - else aux l - in - aux !load_paths - -let expand_path ?root dir = - let rec aux = function - | [] -> [] - | { path_physical = ph; path_logical = lg; path_implicit = implicit } :: l -> - let success = - match root with - | None -> - if implicit then is_dirpath_suffix_of dir lg - else DirPath.equal dir lg - | Some root -> - is_dirpath_prefix_of root lg && - is_dirpath_suffix_of dir (drop_dirpath_prefix root lg) in - if success then (ph, lg) :: aux l else aux l in - aux !load_paths - -let locate_file fname = - let paths = List.map physical !load_paths in - let _,longfname = - System.find_file_in_path ~warn:(not !Flags.quiet) paths fname in - longfname diff --git a/library/nametab.mli b/library/nametab.mli index a4f177aad0..33cb4faf99 100644 --- a/library/nametab.mli +++ b/library/nametab.mli @@ -38,7 +38,7 @@ open Globnames } {- [exists : full_user_name -> bool] - Is the [full_user_name] already atributed as an absolute user name + Is the [full_user_name] already attributed as an absolute user name of some object? } {- [locate : qualid -> object_reference] diff --git a/library/summary.mli b/library/summary.mli index 0d77d725ac..3875bcfe9e 100644 --- a/library/summary.mli +++ b/library/summary.mli @@ -28,7 +28,7 @@ type 'a summary_declaration = { Beware: for tables registered dynamically after the initialization of Coq, their init functions may not be run immediately. It is hence - the responsability of plugins to initialize themselves properly. + the responsibility of plugins to initialize themselves properly. *) val declare_summary : string -> 'a summary_declaration -> unit diff --git a/man/coqdep.1 b/man/coqdep.1 index c417402c25..4639a75677 100644 --- a/man/coqdep.1 +++ b/man/coqdep.1 @@ -106,7 +106,7 @@ Skips subdirectory Output the given file name ordered by dependencies. .TP .B \-boot -For coq developpers, prints dependencies over coq library files +For coq developers, prints dependencies over coq library files (omitted by default). diff --git a/parsing/g_constr.mlg b/parsing/g_constr.mlg index 6df97609f5..bd88570224 100644 --- a/parsing/g_constr.mlg +++ b/parsing/g_constr.mlg @@ -31,8 +31,10 @@ let ldots_var = Id.of_string ".." let constr_kw = [ "forall"; "fun"; "match"; "fix"; "cofix"; "with"; "in"; "for"; "end"; "as"; "let"; "if"; "then"; "else"; "return"; - "SProp"; "Prop"; "Set"; "Type"; ".("; "_"; ".."; - "`{"; "`("; "{|"; "|}" ] + "SProp"; "Prop"; "Set"; "Type"; + ":="; "=>"; "->"; ".."; "<:"; "<<:"; ":>"; + ".("; "()"; "`{"; "`("; "@{"; "{|"; + "_"; "@"; "+"; "!"; "?"; ";"; ","; ":" ] let _ = List.iter CLexer.add_keyword constr_kw @@ -225,11 +227,13 @@ GRAMMAR EXTEND Gram [ c=atomic_constr -> { c } | c=match_constr -> { c } | "("; c = operconstr LEVEL "200"; ")" -> - { (match c.CAst.v with + { (* Preserve parentheses around numerals so that constrintern does not + collapse -(3) into the numeral -3. *) + (match c.CAst.v with | CPrim (Numeral (SPlus,n)) -> CAst.make ~loc @@ CNotation((InConstrEntrySomeLevel,"( _ )"),([c],[],[],[])) | _ -> c) } - | "{|"; c = record_declaration; "|}" -> { c } + | "{|"; c = record_declaration; bar_cbrace -> { c } | "{"; c = binder_constr ; "}" -> { CAst.make ~loc @@ CNotation((InConstrEntrySomeLevel,"{ _ }"),([c],[],[],[])) } | "`{"; c = operconstr LEVEL "200"; "}" -> @@ -277,16 +281,16 @@ GRAMMAR EXTEND Gram ":="; c1 = operconstr LEVEL "200"; "in"; c2 = operconstr LEVEL "200" -> { CAst.make ~loc @@ CLetTuple (lb,po,c1,c2) } - | "let"; "'"; p=pattern; ":="; c1 = operconstr LEVEL "200"; + | "let"; "'"; p = pattern LEVEL "200"; ":="; c1 = operconstr LEVEL "200"; "in"; c2 = operconstr LEVEL "200" -> { CAst.make ~loc @@ CCases (LetPatternStyle, None, [c1, None, None], [CAst.make ~loc ([[p]], c2)]) } - | "let"; "'"; p=pattern; ":="; c1 = operconstr LEVEL "200"; + | "let"; "'"; p = pattern LEVEL "200"; ":="; c1 = operconstr LEVEL "200"; rt = case_type; "in"; c2 = operconstr LEVEL "200" -> { CAst.make ~loc @@ CCases (LetPatternStyle, Some rt, [c1, aliasvar p, None], [CAst.make ~loc ([[p]], c2)]) } - | "let"; "'"; p=pattern; "in"; t = pattern LEVEL "200"; + | "let"; "'"; p = pattern LEVEL "200"; "in"; t = pattern LEVEL "200"; ":="; c1 = operconstr LEVEL "200"; rt = case_type; "in"; c2 = operconstr LEVEL "200" -> { CAst.make ~loc @@ @@ -359,7 +363,7 @@ GRAMMAR EXTEND Gram case_item: [ [ c=operconstr LEVEL "100"; ona = OPT ["as"; id=name -> { id } ]; - ty = OPT ["in"; t=pattern -> { t } ] -> + ty = OPT ["in"; t = pattern LEVEL "200" -> { t } ] -> { (c,ona,ty) } ] ] ; case_type: @@ -377,14 +381,14 @@ GRAMMAR EXTEND Gram [ [ OPT"|"; br=LIST0 eqn SEP "|" -> { br } ] ] ; mult_pattern: - [ [ pl = LIST1 pattern LEVEL "99" SEP "," -> { pl } ] ] + [ [ pl = LIST1 pattern LEVEL "200" SEP "," -> { pl } ] ] ; eqn: [ [ pll = LIST1 mult_pattern SEP "|"; "=>"; rhs = lconstr -> { (CAst.make ~loc (pll,rhs)) } ] ] ; record_pattern: - [ [ id = global; ":="; pat = pattern -> { (id, pat) } ] ] + [ [ id = global; ":="; pat = pattern LEVEL "200" -> { (id, pat) } ] ] ; record_patterns: [ [ p = record_pattern; ";"; ps = record_patterns -> { p :: ps } @@ -396,7 +400,10 @@ GRAMMAR EXTEND Gram pattern: [ "200" RIGHTA [ ] | "100" RIGHTA - [ p = pattern; "|"; pl = LIST1 pattern SEP "|" -> { CAst.make ~loc @@ CPatOr (p::pl) } ] + [ p = pattern; ":"; ty = binder_constr -> + {CAst.make ~loc @@ CPatCast (p, ty) } + | p = pattern; ":"; ty = operconstr LEVEL "100" -> + {CAst.make ~loc @@ CPatCast (p, ty) } ] | "99" RIGHTA [ ] | "90" RIGHTA [ ] | "10" LEFTA @@ -409,21 +416,17 @@ GRAMMAR EXTEND Gram [ c = pattern; "%"; key=IDENT -> { CAst.make ~loc @@ CPatDelimiters (key,c) } ] | "0" [ r = Prim.reference -> { CAst.make ~loc @@ CPatAtom (Some r) } - | "{|"; pat = record_patterns; "|}" -> { CAst.make ~loc @@ CPatRecord pat } + | "{|"; pat = record_patterns; bar_cbrace -> { CAst.make ~loc @@ CPatRecord pat } | "_" -> { CAst.make ~loc @@ CPatAtom None } | "("; p = pattern LEVEL "200"; ")" -> - { (match p.CAst.v with + { (* Preserve parentheses around numerals so that constrintern does not + collapse -(3) into the numeral -3. *) + (match p.CAst.v with | CPatPrim (Numeral (SPlus,n)) -> CAst.make ~loc @@ CPatNotation((InConstrEntrySomeLevel,"( _ )"),([p],[]),[]) | _ -> p) } - | "("; p = pattern LEVEL "200"; ":"; ty = lconstr; ")" -> - { let p = - match p with - | { CAst.v = CPatPrim (Numeral (SPlus,n)) } -> - CAst.make ~loc @@ CPatNotation((InConstrEntrySomeLevel,"( _ )"),([p],[]),[]) - | _ -> p - in - CAst.make ~loc @@ CPatCast (p, ty) } + | "("; p = pattern LEVEL "200"; "|" ; pl = LIST1 pattern LEVEL "200" SEP "|"; ")" -> + { CAst.make ~loc @@ CPatOr (p::pl) } | n = NUMERAL-> { CAst.make ~loc @@ CPatPrim (Numeral (SPlus,n)) } | s = string -> { CAst.make ~loc @@ CPatPrim (String s) } ] ] ; diff --git a/parsing/g_prim.mlg b/parsing/g_prim.mlg index 80dd997860..9653964262 100644 --- a/parsing/g_prim.mlg +++ b/parsing/g_prim.mlg @@ -15,7 +15,7 @@ open Libnames open Pcoq.Prim -let prim_kw = ["{"; "}"; "["; "]"; "("; ")"; "'"] +let prim_kw = ["{"; "}"; "["; "]"; "("; ")"; "'"; "%"; "|"] let _ = List.iter CLexer.add_keyword prim_kw @@ -31,13 +31,19 @@ let my_int_of_string loc s = with Failure _ -> CErrors.user_err ~loc (Pp.str "This number is too large.") +let check_nospace loc expected = + let (bp, ep) = Loc.unloc loc in + if ep = bp + String.length expected then () else + Gramlib.Ploc.raise loc (Stream.Error ("'" ^ expected ^ "' expected")) + } GRAMMAR EXTEND Gram GLOBAL: bigint natural integer identref name ident var preident fullyqualid qualid reference dirpath ne_lstring - ne_string string lstring pattern_ident pattern_identref by_notation smart_global; + ne_string string lstring pattern_ident pattern_identref by_notation + smart_global bar_cbrace; preident: [ [ s = IDENT -> { s } ] ] ; @@ -123,4 +129,7 @@ GRAMMAR EXTEND Gram bigint: (* Negative numbers are dealt with elsewhere *) [ [ i = NUMERAL -> { check_int loc i } ] ] ; + bar_cbrace: + [ [ "|"; "}" -> { check_nospace loc "|}" } ] ] + ; END diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index 8f38e437b4..b474c8e9a9 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -411,6 +411,8 @@ module Prim = let ne_string = Entry.create "Prim.ne_string" let ne_lstring = Entry.create "Prim.ne_lstring" + let bar_cbrace = Entry.create "'|}'" + end module Constr = @@ -585,7 +587,7 @@ let unfreeze (grams, lex) = (** No need to provide an init function : the grammar state is statically available, and already empty initially, while - the lexer state should not be resetted, since it contains + the lexer state should not be reset, since it contains keywords declared in g_*.ml4 *) let parser_summary_tag = diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 3a57c14a3b..5f982346ab 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -38,9 +38,9 @@ end - dynamic rules declared at the evaluation of Coq files (using e.g. Notation, Infix, or Tactic Notation) - - static rules explicitly defined in files g_*.ml4 + - static rules explicitly defined in files g_*.mlg - static rules macro-generated by ARGUMENT EXTEND, TACTIC EXTEND and - VERNAC EXTEND (see e.g. file extratactics.ml4) + VERNAC EXTEND (see e.g. file extratactics.mlg) Note that parsing a Coq document is in essence stateful: the parser needs to recognize commands that start proofs and use a different @@ -170,6 +170,7 @@ module Prim : val ne_string : string Entry.t val ne_lstring : lstring Entry.t val var : lident Entry.t + val bar_cbrace : unit Entry.t end module Constr : diff --git a/plugins/extraction/CHANGES b/plugins/extraction/CHANGES index 4bc3dba36e..bc7e1448f7 100644 --- a/plugins/extraction/CHANGES +++ b/plugins/extraction/CHANGES @@ -200,7 +200,7 @@ For the moment there are: Wf.well_founded_induction Wf.well_founded_induction_type Those constants does not match the auto-inlining criterion based on strictness. -Of course, you can still overide this behaviour via some Extraction NoInline. +Of course, you can still override this behaviour via some Extraction NoInline. * There is now a web page showing the extraction of all standard theories: http://www.lri.fr/~letouzey/extraction diff --git a/plugins/extraction/ExtrOcamlBasic.v b/plugins/extraction/ExtrOcamlBasic.v index 36bb1148b6..02da168fd0 100644 --- a/plugins/extraction/ExtrOcamlBasic.v +++ b/plugins/extraction/ExtrOcamlBasic.v @@ -26,9 +26,9 @@ Extract Inductive prod => "( * )" [ "" ]. Extract Inductive sumbool => bool [ true false ]. Extract Inductive sumor => option [ Some None ]. -(** Restore lazyness of andb, orb. +(** Restore laziness of andb, orb. NB: without these Extract Constant, andb/orb would be inlined - by extraction in order to have lazyness, producing inelegant + by extraction in order to have laziness, producing inelegant (if ... then ... else false) and (if ... then true else ...). *) diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml index 59c57cc544..f46d09e335 100644 --- a/plugins/extraction/common.ml +++ b/plugins/extraction/common.ml @@ -573,7 +573,7 @@ let pp_ocaml_gen k mp rls olab = if is_mp_bound base then pp_ocaml_bound base rls else pp_ocaml_extern k base rls -(* For Haskell, things are simplier: we have removed (almost) all structures *) +(* For Haskell, things are simpler: we have removed (almost) all structures *) let pp_haskell_gen k mp rls = match rls with | [] -> assert false @@ -590,7 +590,7 @@ let pp_global k r = let s = List.hd ls in let mp,l = repr_of_r r in if ModPath.equal mp (top_visible_mp ()) then - (* simpliest situation: definition of r (or use in the same context) *) + (* simplest situation: definition of r (or use in the same context) *) (* we update the visible environment *) (add_visible (k,s) l; unquote s) else @@ -607,7 +607,7 @@ let pp_module mp = let ls = mp_renaming mp in match mp with | MPdot (mp0,l) when ModPath.equal mp0 (top_visible_mp ()) -> - (* simpliest situation: definition of mp (or use in the same context) *) + (* simplest situation: definition of mp (or use in the same context) *) (* we update the visible environment *) let s = List.hd ls in add_visible (Mod,s) l; s diff --git a/plugins/extraction/g_extraction.mlg b/plugins/extraction/g_extraction.mlg index d7bb27f121..db1a389fe7 100644 --- a/plugins/extraction/g_extraction.mlg +++ b/plugins/extraction/g_extraction.mlg @@ -93,7 +93,7 @@ VERNAC COMMAND EXTEND Extraction CLASSIFIED AS QUERY END VERNAC COMMAND EXTEND SeparateExtraction CLASSIFIED AS QUERY -(* Same, with content splitted in several files *) +(* Same, with content split in several files *) | [ "Separate" "Extraction" ne_global_list(l) ] -> { separate_extraction l } END diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index 4e229a94b6..c2c48f9565 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -101,7 +101,7 @@ let labels_of_ref r = (*S The main tables: constants, inductives, records, ... *) -(* Theses tables are not registered within coq save/undo mechanism +(* These tables are not registered within coq save/undo mechanism since we reset their contents at each run of Extraction *) (* We use [constant_body] (resp. [mutual_inductive_body]) as checksum @@ -842,7 +842,7 @@ let in_customs : GlobRef.t * string list * string -> obj = ~subst:(Some (fun (s,(r,ids,str)) -> (fst (subst_global s r), ids, str))) let in_custom_matchs : GlobRef.t * string -> obj = - declare_object @@ superglobal_object_nodischarge "ML extractions custom matchs" + declare_object @@ superglobal_object_nodischarge "ML extractions custom matches" ~cache:(fun (_,(r,s)) -> add_custom_match r s) ~subst:(Some (fun (subs,(r,s)) -> (fst (subst_global subs r), s))) diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 287a374ab1..cffe8a3e78 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -658,7 +658,7 @@ let instantiate_hyps_with_args (do_prove:Id.t list -> tactic) hyps args_id = *) (fun g -> -(* observe (str "Instanciation: removing hyp " ++ Ppconstr.pr_id hid); *) +(* observe (str "Instantiation: removing hyp " ++ Ppconstr.pr_id hid); *) thin [hid] g ) ) diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index e9a2c285d0..f51c6dc6be 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -429,11 +429,11 @@ let get_funs_constant mp = let l_const = get_funs_constant const f in (* We need to check that all the functions found are in the same block - to prevent Reset stange thing + to prevent Reset strange thing *) let l_bodies = List.map find_constant_body (Array.to_list (Array.map fst l_const)) in let l_params,l_fixes = List.split (List.map decompose_lam l_bodies) in - (* all the paremeter must be equal*) + (* all the parameters must be equal*) let _check_params = let first_params = List.hd l_params in List.iter @@ -514,7 +514,7 @@ let make_scheme evd (fas : (pconstant*Sorts.family) list) : Safe_typing.private_ ) fas in - (* We create the first priciple by tactic *) + (* We create the first principle by tactic *) let first_type,other_princ_types = match l_schemes with s::l_schemes -> s,l_schemes diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index e15e167ff3..4c67d65816 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -1369,7 +1369,7 @@ let do_build_inductive (rebuild_return_type returned_types.(i)) in (* We need to lift back our work topconstr but only with all information - We mimick a Set Printing All. + We mimic a Set Printing All. Then save the graphs and reset Printing options to their primitive values *) let rel_arities = Array.mapi rel_arity funsargs in @@ -1438,7 +1438,7 @@ let do_build_inductive (rebuild_return_type returned_types.(i)) in (* We need to lift back our work topconstr but only with all information - We mimick a Set Printing All. + We mimic a Set Printing All. Then save the graphs and reset Printing options to their primitive values *) let rel_arities = Array.mapi rel_arity funsargs in diff --git a/plugins/funind/glob_termops.mli b/plugins/funind/glob_termops.mli index 481a8be3ba..24b3690138 100644 --- a/plugins/funind/glob_termops.mli +++ b/plugins/funind/glob_termops.mli @@ -55,7 +55,7 @@ val change_vars : Id.t Id.Map.t -> glob_constr -> glob_constr Glob_term.cases_pattern * Id.Map.key list * Id.t Id.Map.t -(* [alpha_rt avoid rt] alpha convert [rt] s.t. the result repects barendregt +(* [alpha_rt avoid rt] alpha convert [rt] s.t. the result respects barendregt conventions and does not share bound variables with avoid *) val alpha_rt : Id.t list -> glob_constr -> glob_constr diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 40f66ce5eb..48cf040919 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -115,7 +115,7 @@ let eq = lazy(EConstr.of_constr (coq_constant "eq")) let refl_equal = lazy(EConstr.of_constr (coq_constant "eq_refl")) (*****************************************************************) -(* Copy of the standart save mechanism but without the much too *) +(* Copy of the standard save mechanism but without the much too *) (* slow reduction function *) (*****************************************************************) open Entries @@ -357,7 +357,7 @@ let add_Function is_general f = let pr_table env sigma = pr_table env sigma !from_function (*********************************) -(* Debuging *) +(* Debugging *) let functional_induction_rewrite_dependent_proofs = ref true let function_debug = ref false open Goptions diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index edb698280f..2a0140f02c 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -591,7 +591,7 @@ let rec reflexivity_with_destruct_cases g = (* [prove_fun_complete funs graphs schemes lemmas_types_infos i] - is the tactic used to prove completness lemma. + is the tactic used to prove completeness lemma. [funcs], [graphs] [schemes] [lemmas_types_infos] are the mutually recursive functions (resp. definitions of the graphs of the functions, principles and correctness lemma types) to prove correct. @@ -748,7 +748,7 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list let funs = Array.of_list funs and graphs = Array.of_list graphs in let map (c, u) = mkConstU (c, EInstance.make u) in let funs_constr = Array.map map funs in - (* XXX STATE Why do we need this... why is the toplevel protection not enought *) + (* XXX STATE Why do we need this... why is the toplevel protection not enough *) funind_purify (fun () -> let env = Global.env () in @@ -928,7 +928,7 @@ let revert_graph kn post_tac hid g = [hid] is the hypothesis to invert, [fconst] is the function to invert and [f_correct] is the correctness lemma for [fconst]. - The sketch is the follwing~: + The sketch is the following~: \begin{enumerate} \item Transforms the hypothesis [hid] such that its type is now $res\ =\ f\ t_1 \ldots t_n$ (fails if it is not possible) diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 1fca132655..216be3797b 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1584,7 +1584,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num spc () ++ str"is defined" ) ) in - (* XXX STATE Why do we need this... why is the toplevel protection not enought *) + (* XXX STATE Why do we need this... why is the toplevel protection not enough *) funind_purify (fun () -> let pstate = com_terminate tcc_lemma_name diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 963b7189f9..164bd7e118 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -30,7 +30,6 @@ open Evd open Tactypes open Locus open Locusops -open Decl_kinds open Elimschemes open Environ open Termops @@ -207,7 +206,7 @@ end) = struct let mk_relation env evd a = app_poly env evd relation [| a |] - (** Build an infered signature from constraints on the arguments and expected output + (** Build an inferred signature from constraints on the arguments and expected output relation *) let build_signature evars env m (cstrs : (types * types option) option list) @@ -1791,15 +1790,15 @@ let rec strategy_of_ast = function let mkappc s l = CAst.make @@ CAppExpl ((None,qualid_of_ident (Id.of_string s),None),l) let declare_an_instance n s args = - (((CAst.make @@ Name n),None), Explicit, + (((CAst.make @@ Name n),None), CAst.make @@ CAppExpl ((None, qualid_of_string s,None), args)) let declare_instance a aeq n s = declare_an_instance n s [a;aeq] -let anew_instance ~pstate atts binders instance fields = +let anew_instance ~pstate atts binders (name,t) fields = let program_mode = atts.program in new_instance ~pstate ~program_mode atts.polymorphic - binders instance (Some (true, CAst.make @@ CRecord (fields))) + name binders t (Some (true, CAst.make @@ CRecord (fields))) ~global:atts.global ~generalize:false Hints.empty_hint_info let declare_instance_refl ~pstate atts binders a aeq n lemma = @@ -2014,16 +2013,18 @@ let add_morphism_infer ~pstate atts m n : Proof_global.t option = let add_morphism ~pstate atts binders m s n = init_setoid (); let instance_id = add_suffix n "_Proper" in - let instance = - (((CAst.make @@ Name instance_id),None), Explicit, - CAst.make @@ CAppExpl ( - (None, Libnames.qualid_of_string "Coq.Classes.Morphisms.Proper",None), - [cHole; s; m])) + let instance_name = (CAst.make @@ Name instance_id),None in + let instance_t = + CAst.make @@ CAppExpl + ((None, Libnames.qualid_of_string "Coq.Classes.Morphisms.Proper",None), + [cHole; s; m]) in let tac = Tacinterp.interp (make_tactic "add_morphism_tactic") in - let _, pstate = new_instance ~pstate ~program_mode:atts.program ~global:atts.global atts.polymorphic binders instance - None - ~generalize:false ~tac ~hook:(declare_projection n instance_id) Hints.empty_hint_info in + let _, pstate = new_instance ~pstate + ~program_mode:atts.program ~global:atts.global atts.polymorphic + instance_name binders instance_t None + ~generalize:false ~tac ~hook:(declare_projection n instance_id) Hints.empty_hint_info + in pstate (** Bind to "rewrite" too *) diff --git a/plugins/ltac/tacexpr.ml b/plugins/ltac/tacexpr.ml index 0eb7726a18..8bd69dd4fd 100644 --- a/plugins/ltac/tacexpr.ml +++ b/plugins/ltac/tacexpr.ml @@ -24,7 +24,7 @@ type direction_flag = bool (* true = Left-to-right false = right-to-right *) type lazy_flag = | General (* returns all possible successes *) | Select (* returns all successes of the first matching branch *) - | Once (* returns the first success in a maching branch + | Once (* returns the first success in a matching branch (not necessarily the first) *) type global_flag = (* [gfail] or [fail] *) | TacGlobal diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli index fd303f5d94..f839c3e886 100644 --- a/plugins/ltac/tacexpr.mli +++ b/plugins/ltac/tacexpr.mli @@ -24,7 +24,7 @@ type direction_flag = bool (* true = Left-to-right false = right-to-right *) type lazy_flag = | General (* returns all possible successes *) | Select (* returns all successes of the first matching branch *) - | Once (* returns the first success in a maching branch + | Once (* returns the first success in a matching branch (not necessarily the first) *) type global_flag = (* [gfail] or [fail] *) | TacGlobal diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 800be2565d..4a0b01bcdc 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -855,7 +855,7 @@ let interp_binding_name ist env sigma = function | NamedHyp id -> (* If a name is bound, it has to be a quantified hypothesis *) (* user has to use other names for variables if these ones clash with *) - (* a name intented to be used as a (non-variable) identifier *) + (* a name intended to be used as a (non-variable) identifier *) try try_interp_ltac_var (coerce_to_quantified_hypothesis sigma) ist (Some (env,sigma)) (make id) with Not_found -> NamedHyp id @@ -2075,7 +2075,7 @@ let _ = let extra = TacStore.set TacStore.empty f_debug (get_debug ()) in let ist = { lfun; poly; extra; } in let tac = interp_tactic ist tac in - (* EJGA: We sould also pass the proof name if desired, for now + (* EJGA: We should also pass the proof name if desired, for now poly seems like enough to get reasonable behavior in practice *) let name, poly = Id.of_string "ltac_gen", poly in diff --git a/plugins/ltac/tactic_matching.ml b/plugins/ltac/tactic_matching.ml index 2b5e496168..7783661787 100644 --- a/plugins/ltac/tactic_matching.ml +++ b/plugins/ltac/tactic_matching.ml @@ -128,7 +128,7 @@ module PatternMatching (E:StaticEnvironment) = struct (** To focus on the algorithmic portion of pattern-matching, the bookkeeping is relegated to a monad: the composition of the - bactracking monad of {!IStream.t} with a "writer" effect. *) + backtracking monad of {!IStream.t} with a "writer" effect. *) (* spiwack: as we don't benefit from the various stream optimisations of Haskell, it may be costly to give the monad in direct style such as here. We may want to use some continuation passing style. *) diff --git a/plugins/micromega/OrderedRing.v b/plugins/micromega/OrderedRing.v index e0e2232be5..7759bda7c7 100644 --- a/plugins/micromega/OrderedRing.v +++ b/plugins/micromega/OrderedRing.v @@ -129,7 +129,7 @@ Proof. intros n m H1 H2; rewrite H2 in H1; now apply H1. Qed. -(* Propeties of plus, minus and opp *) +(* Properties of plus, minus and opp *) Theorem Rplus_0_l : forall n : R, 0 + n == n. Proof. diff --git a/plugins/micromega/RingMicromega.v b/plugins/micromega/RingMicromega.v index 60931df517..c5e179fbb8 100644 --- a/plugins/micromega/RingMicromega.v +++ b/plugins/micromega/RingMicromega.v @@ -990,7 +990,7 @@ Proof. rewrite IHs. reflexivity. Qed. -(** equality migth be (too) strong *) +(** equality might be (too) strong *) Lemma eval_formulaSC : forall env f, eval_sformula env f = eval_formula env (map_Formula f). Proof. destruct f. diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index bed9e55ac0..48027442b2 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -1208,8 +1208,8 @@ let dump_rexpr = lazy (** [make_goal_of_formula depxr vars props form] where - - vars is an environment for the arithmetic variables occuring in form - - props is an environment for the propositions occuring in form + - vars is an environment for the arithmetic variables occurring in form + - props is an environment for the propositions occurring in form @return a goal where all the variables and propositions of the formula are quantified *) @@ -1469,7 +1469,7 @@ let pre_processZ mt f = x <= y or (x and y are incomparable) *) (** - * Instanciate the current Coq goal with a Micromega formula, a varmap, and a + * Instantiate the current Coq goal with a Micromega formula, a varmap, and a * witness. *) diff --git a/plugins/micromega/persistent_cache.ml b/plugins/micromega/persistent_cache.ml index 0209030b64..f038f8a71a 100644 --- a/plugins/micromega/persistent_cache.ml +++ b/plugins/micromega/persistent_cache.ml @@ -21,7 +21,7 @@ module type PHashtable = val open_in : string -> 'a t (** [open_in f] rebuilds a table from the records stored in file [f]. - As marshaling is not type-safe, it migth segault. + As marshaling is not type-safe, it might segfault. *) val find : 'a t -> key -> 'a diff --git a/plugins/micromega/persistent_cache.mli b/plugins/micromega/persistent_cache.mli index 4e7a388aaf..d2f3e756a9 100644 --- a/plugins/micromega/persistent_cache.mli +++ b/plugins/micromega/persistent_cache.mli @@ -17,7 +17,7 @@ module type PHashtable = val open_in : string -> 'a t (** [open_in f] rebuilds a table from the records stored in file [f]. - As marshaling is not type-safe, it migth segault. + As marshaling is not type-safe, it might segfault. *) val find : 'a t -> key -> 'a diff --git a/plugins/micromega/sos_lib.ml b/plugins/micromega/sos_lib.ml index 6aebc4ca9a..e3a9f6f60f 100644 --- a/plugins/micromega/sos_lib.ml +++ b/plugins/micromega/sos_lib.ml @@ -200,7 +200,7 @@ let is_undefined f = | _ -> false;; (* ------------------------------------------------------------------------- *) -(* Operation analagous to "map" for lists. *) +(* Operation analogous to "map" for lists. *) (* ------------------------------------------------------------------------- *) let mapf = diff --git a/plugins/nsatz/nsatz.ml b/plugins/nsatz/nsatz.ml index 1777418ef6..bece316c7d 100644 --- a/plugins/nsatz/nsatz.ml +++ b/plugins/nsatz/nsatz.ml @@ -267,7 +267,7 @@ module PIdeal = Ideal.Make(Poly) open PIdeal (* term to sparse polynomial - varaibles <=np are in the coefficients + variables <=np are in the coefficients *) let term_pol_sparse nvars np t= diff --git a/plugins/nsatz/polynom.ml b/plugins/nsatz/polynom.ml index 5db587b9cc..f6ca232c2e 100644 --- a/plugins/nsatz/polynom.ml +++ b/plugins/nsatz/polynom.ml @@ -357,7 +357,7 @@ let remP v p = moinsP p (multP (coefDom v p) (puisP (x v) (deg v p))) -(* first interger coefficient of p *) +(* first integer coefficient of p *) let rec coef_int_tete p = let v = max_var_pol p in if v>0 @@ -526,7 +526,7 @@ let div_pol_rat p q= (* pseudo division : q = c*x^m+q1 - retruns (r,c,d,s) s.t. c^d*p = s*q + r. + returns (r,c,d,s) s.t. c^d*p = s*q + r. *) let pseudo_div p q x = diff --git a/plugins/ssr/ssrbool.v b/plugins/ssr/ssrbool.v index 49d729bd6c..c5f387b248 100644 --- a/plugins/ssr/ssrbool.v +++ b/plugins/ssr/ssrbool.v @@ -49,7 +49,7 @@ Require Import ssreflect ssrfun. altP (idP my_formula) but circumventing the dependent index capture issue; destructing boolP my_formula generates two subgoals with - assumtions my_formula and ~~ myformula. As + assumptions my_formula and ~~ myformula. As with altP, my_formula must be an application. \unless C, P <-> we can assume property P when a something that holds under condition C (such as C itself). @@ -64,7 +64,7 @@ Require Import ssreflect ssrfun. := forall b : bool, (P -> b) -> b. This is equivalent to ~ (~ P) when P : Prop. implies P Q == wrapper variant type that coerces to P -> Q and - can be used as a P -> Q view unambigously. + can be used as a P -> Q view unambiguously. Useful to avoid spurious insertion of <-> views when Q is a conjunction of foralls, as in Lemma all_and2 below; conversely, avoids confusion in @@ -1003,7 +1003,7 @@ Proof. by case: a; case: b. Qed. Lemma negb_or (a b : bool) : ~~ (a || b) = ~~ a && ~~ b. Proof. by case: a; case: b. Qed. -(** Pseudo-cancellation -- i.e, absorbtion **) +(** Pseudo-cancellation -- i.e, absorption **) Lemma andbK a b : a && b || a = a. Proof. by case: a; case: b. Qed. Lemma andKb a b : a || b && a = a. Proof. by case: a; case: b. Qed. @@ -1245,7 +1245,7 @@ Notation "[ 'pred' x : T | E1 & E2 ]" := (** Coercions for simpl_pred. As simpl_pred T values are used both applicatively and collectively we need simpl_pred to coerce to both pred T _and_ {pred T}. However it is - undesireable to have two distinct constants for what are essentially identical + undesirable to have two distinct constants for what are essentially identical coercion functions, as this confuses the SSReflect keyed matching algorithm. While the Coq Coercion declarations appear to disallow such Coercion aliasing, it is possible to work around this limitation with a combination of modules @@ -1331,9 +1331,9 @@ Variant mem_pred T := Mem of pred T. Similarly to pred_of_simpl, it will usually not be inserted by type inference, as all mem_pred mp =~= pred_sort ?pT unification problems will be solve by the memPredType instance below; pred_of_mem will however - be used if a mem_pred T is used as a {pred T}, which is desireable as it + be used if a mem_pred T is used as a {pred T}, which is desirable as it will avoid a redundant mem in a collective, e.g., passing (mem A) to a lemma - expection a generic collective predicate p : {pred T} and premise x \in P + exception a generic collective predicate p : {pred T} and premise x \in P will display a subgoal x \in A rathere than x \in mem A. Conversely, pred_of_mem will _not_ if it is used id (mem A) is used applicatively or as a pred T; there the simpl_of_mem coercion defined below @@ -1396,7 +1396,7 @@ Notation "[ 'rel' x y 'in' A & B ]" := Notation "[ 'rel' x y 'in' A | E ]" := [rel x y in A & A | E] : fun_scope. Notation "[ 'rel' x y 'in' A ]" := [rel x y in A & A] : fun_scope. -(** Aliases of pred T that let us tag intances of simpl_pred as applicative +(** Aliases of pred T that let us tag instances of simpl_pred as applicative or collective, via bespoke coercions. This tagging will give control over the simplification behaviour of inE and othe rewriting lemmas below. For this control to work it is crucial that collective_of_simpl _not_ @@ -1428,7 +1428,7 @@ Implicit Types (mp : mem_pred T). - registered_applicative_pred: this user-facing structure is used to declare values of type pred T meant to be used applicatively. The structure parameter merely displays this same value, and is used to avoid - undesireable, visible occurrence of the structure in the right hand side + undesirable, visible occurrence of the structure in the right hand side of rewrite rules such as app_predE. There is a canonical instance of registered_applicative_pred for values of the applicative_of_simpl coercion, which handles the @@ -1454,7 +1454,7 @@ Implicit Types (mp : mem_pred T). has been fixed earlier by the manifest_mem_pred match. In particular the definition of a predicate using the applicative_pred_of_simpl idiom above will not be expanded - this very case is the reason in_applicative uses - a mem_pred telescope in its left hand side. The more straighforward + a mem_pred telescope in its left hand side. The more straightforward ?x \in applicative_pred_value ?ap (equivalent to in_mem ?x (Mem ?ap)) with ?ap : registered_applicative_pred ?p would set ?p := [pred x | ...] rather than ?p := Apred in the example above. diff --git a/plugins/ssr/ssreflect.v b/plugins/ssr/ssreflect.v index 5e3e8ce5fb..572d72ccd8 100644 --- a/plugins/ssr/ssreflect.v +++ b/plugins/ssr/ssreflect.v @@ -132,7 +132,7 @@ Delimit Scope ssripat_scope with ssripat. Make the general "if" into a notation, so that we can override it below. The notations are "only parsing" because the Coq decompiler will not recognize the expansion of the boolean if; using the default printer - avoids a spurrious trailing %%GEN_IF. **) + avoids a spurious trailing %%GEN_IF. **) Declare Scope general_if_scope. Delimit Scope general_if_scope with GEN_IF. @@ -347,10 +347,10 @@ Register protect_term as plugins.ssreflect.protect_term. (** The ssreflect idiom for a non-keyed pattern: - - unkeyed t wiil match any subterm that unifies with t, regardless of + - unkeyed t will match any subterm that unifies with t, regardless of whether it displays the same head symbol as t. - unkeyed t a b will match any application of a term f unifying with t, - to two arguments unifying with with a and b, repectively, regardless of + to two arguments unifying with with a and b, respectively, regardless of apparent head symbols. - unkeyed x where x is a variable will match any subterm with the same type as x (when x would raise the 'indeterminate pattern' error). **) @@ -380,7 +380,7 @@ Notation "=^~ r" := (ssr_converse r) : form_scope. locked_with k t is equal but not convertible to t, much like locked t, but supports explicit tagging with a value k : unit. This is used to mitigate a flaw in the term comparison heuristic of the Coq kernel, - which treats all terms of the form locked t as equal and conpares their + which treats all terms of the form locked t as equal and compares their arguments recursively, leading to an exponential blowup of comparison. For this reason locked_with should be used rather than locked when defining ADT operations. The unlock tactic does not support locked_with @@ -523,7 +523,7 @@ Hint View for apply/ iffRLn|2 iffLRn|2 iffRL|2 iffLR|2. elim/abstract_context: (pattern) => G defG. vm_compute; rewrite {}defG {G}. Note that vm_cast are not stored in the proof term - for reductions occuring in the context, hence + for reductions occurring in the context, hence set here := pattern; vm_compute in (value of here) blows up at Qed time. **) Lemma abstract_context T (P : T -> Type) x : @@ -637,7 +637,7 @@ Ltac over := later complain that it cannot erase _top_assumption_ after having abstracted the viewed assumption. Making x and y maximal implicits would avoid this and force the intended @Some_inj nat x y _top_assumption_ - interpretation, but is undesireable as it makes it harder to use Some_inj + interpretation, but is undesirable as it makes it harder to use Some_inj with the many SSReflect and MathComp lemmas that have an injectivity premise. Specifying {T : nonPropType} solves this more elegantly, as then (?T : Type) no longer unifies with (Some n = Some 0), which has sort Prop. @@ -655,13 +655,13 @@ Module NonPropType. maybeProp T to tt and use the test_negative instance and set ?r to false. - call_of c r sets up a call to test_of on condition c with expected result r. It has a default instance for its 'callee' projection to Type, which - sets c := maybeProj T and r := false whe unifying with a type T. + sets c := maybeProj T and r := false when unifying with a type T. - type is a telescope on call_of c r, which checks that unifying test_of ?r1 with c indeed sets ?r1 := r; the type structure bundles the 'test' instance and its 'result' value along with its call_of c r projection. The default instance essentially provides eta-expansion for 'type'. This is only essential for the first 'result' projection to bool; using the instance - for other projection merely avoids spurrious delta expansions that would + for other projection merely avoids spurious delta expansions that would spoil the notProp T notation. In detail, unifying T =~= ?S with ?S : nonPropType, i.e., (1) T =~= @callee (@condition (result ?S) (test ?S)) (result ?S) (frame ?S) diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml index 675e4d2457..dbc9bb24c5 100644 --- a/plugins/ssr/ssrelim.ml +++ b/plugins/ssr/ssrelim.ml @@ -96,7 +96,7 @@ let subgoals_tys sigma (relctx, concl) = * (occ, c), deps and the pattern inferred from the type of the eliminator * 3. build the new predicate matching the patterns, and the tactic to * generalize the equality in case eqid is not None - * 4. build the tactic handle intructions and clears as required in ipats and + * 4. build the tactic handle instructions and clears as required in ipats and * by eqid *) let get_eq_type gl = diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index 93c0d5c236..59fc69f100 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -128,7 +128,7 @@ let newssrcongrtac arg ist gl = x, re_sig si sigma in let arr, gl = pf_mkSsrConst "ssr_congr_arrow" gl in let ssr_congr lr = EConstr.mkApp (arr, lr) in - (* here thw two cases: simple equality or arrow *) + (* here the two cases: simple equality or arrow *) let equality, _, eq_args, gl' = let eq, gl = pf_fresh_global Coqlib.(lib_ref "core.eq.type") gl in pf_saturate gl (EConstr.of_constr eq) 3 in @@ -313,7 +313,7 @@ let rw_progress rhs lhs ise = not (EConstr.eq_constr ise lhs (Evarutil.nf_evar i (* Coq has a more general form of "equation" (any type with a single *) (* constructor with no arguments with_rect_r elimination lemmas). *) (* However there is no clear way of determining the LHS and RHS of *) -(* such a generic Leibnitz equation -- short of inspecting the type *) +(* such a generic Leibniz equation -- short of inspecting the type *) (* of the elimination lemmas. *) let rec strip_prod_assum c = match Constr.kind c with diff --git a/plugins/ssrmatching/ssrmatching.mli b/plugins/ssrmatching/ssrmatching.mli index 25975c84e8..6d1d858648 100644 --- a/plugins/ssrmatching/ssrmatching.mli +++ b/plugins/ssrmatching/ssrmatching.mli @@ -143,7 +143,7 @@ val mk_tpattern : type find_P = env -> constr -> int -> k:subst -> constr -(** [conclude ()] asserts that all mentioned ocurrences have been visited. +(** [conclude ()] asserts that all mentioned occurrences have been visited. @return the instance of the pattern, the evarmap after the pattern instantiation, the proof term and the ssrdit stored in the tpattern @raise UserEerror if too many occurrences were specified *) diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index 9d3ed40f6c..e2a63a4540 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -249,7 +249,7 @@ let tag_var = tag Tag.variable str"@{" ++ hov 0 (prlist_with_sep pr_semicolon f (List.rev l)) ++ str"}")) let las = lapp - let lpator = 100 + let lpator = 0 let lpatrec = 0 let rec pr_patt sep inh p = @@ -283,7 +283,8 @@ let tag_var = tag Tag.variable pr_reference r, latom | CPatOr pl -> - hov 0 (prlist_with_sep pr_spcbar (pr_patt mt (lpator,L)) pl), lpator + let pp = pr_patt mt (lpator,Any) in + surround (hov 0 (prlist_with_sep pr_spcbar pp pl)), lpator | CPatNotation ((_,"( _ )"),([p],[]),[]) -> pr_patt (fun()->str"(") (max_int,E) p ++ str")", latom diff --git a/stm/stm.ml b/stm/stm.ml index 6f7cefb582..d469994f3f 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -100,6 +100,15 @@ let forward_feedback, forward_feedback_hook = let unreachable_state, unreachable_state_hook = Hook.make ~default:(fun ~doc:_ _ _ -> ()) () +let document_add, document_add_hook = Hook.make + ~default:(fun _ _ -> ()) () + +let document_edit, document_edit_hook = Hook.make + ~default:(fun _ -> ()) () + +let sentence_exec, sentence_exec_hook = Hook.make + ~default:(fun _ -> ()) () + include Hook (* enables: Hooks.(call foo args) *) @@ -571,7 +580,7 @@ end = struct (* {{{ *) (match Vernacprop.under_control x with | VernacDefinition (_,({CAst.v=Name i},_),_) -> Id.to_string i | VernacStartTheoremProof (_,[({CAst.v=i},_),_]) -> Id.to_string i - | VernacInstance (_,(({CAst.v=Name i},_),_,_),_,_) -> Id.to_string i + | VernacInstance (({CAst.v=Name i},_),_,_,_,_) -> Id.to_string i | _ -> "branch") let edit_branch = Branch.make "edit" let branch ?root ?pos name kind = vcs := branch !vcs ?root ?pos name kind @@ -2661,7 +2670,7 @@ type stm_init_options = { (* Initial load path in scope for the document. Usually extracted from -R options / _CoqProject *) - iload_path : Mltop.coq_path list; + iload_path : Loadpath.coq_path list; (* Require [require_libs] before the initial state is ready. Parameters follow [Library], that is to say, @@ -2719,7 +2728,7 @@ let new_doc { doc_type ; iload_path; require_libs; stm_options } = (* Set load path; important, this has to happen before we declare the library below as [Declaremods/Library] will infer the module name by looking at the load path! *) - List.iter Mltop.add_coq_path iload_path; + List.iter Loadpath.add_coq_path iload_path; Safe_typing.allow_delayed_constants := !cur_opt.async_proofs_mode <> APoff; @@ -2767,6 +2776,7 @@ let new_doc { doc_type ; iload_path; require_libs; stm_options } = doc, VCS.cur_tip () let observe ~doc id = + Hooks.(call sentence_exec id); let vcs = VCS.backup () in try Reach.known_state ~doc ~cache:(VCS.is_interactive ()) id; @@ -3122,6 +3132,7 @@ let compute_indentation ?loc sid = Option.cata (fun loc -> ) (0, 0) loc let add ~doc ~ontop ?newtip verb ast = + Hooks.(call document_add ast ontop); let loc = ast.CAst.loc in let cur_tip = VCS.cur_tip () in if not (Stateid.equal ontop cur_tip) then @@ -3167,6 +3178,7 @@ let query ~doc ~at ~route s = s let edit_at ~doc id = + Hooks.(call document_edit id); if Stateid.equal id Stateid.dummy then anomaly(str"edit_at dummy.") else let vcs = VCS.backup () in let on_cur_branch id = @@ -3322,6 +3334,9 @@ let state_computed_hook = Hooks.state_computed_hook let state_ready_hook = Hooks.state_ready_hook let forward_feedback_hook = Hooks.forward_feedback_hook let unreachable_state_hook = Hooks.unreachable_state_hook +let document_add_hook = Hooks.document_add_hook +let document_edit_hook = Hooks.document_edit_hook +let sentence_exec_hook = Hooks.sentence_exec_hook let () = Hook.set Obligations.stm_get_fix_exn (fun () -> !State.fix_exn_ref) type document = VCS.vcs diff --git a/stm/stm.mli b/stm/stm.mli index 9d2bf56629..24c672c973 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -69,7 +69,7 @@ type stm_init_options = { (* Initial load path in scope for the document. Usually extracted from -R options / _CoqProject *) - iload_path : Mltop.coq_path list; + iload_path : Loadpath.coq_path list; (* Require [require_libs] before the initial state is ready. Parameters follow [Library], that is to say, @@ -282,6 +282,19 @@ val state_ready_hook : (doc:doc -> Stateid.t -> unit) Hook.t (* Messages from the workers to the master *) val forward_feedback_hook : (Feedback.feedback -> unit) Hook.t +(* + * Hooks into the UI for plugins (not for general use) + *) + +(** User adds a sentence to the document (after parsing) *) +val document_add_hook : (Vernacexpr.vernac_control -> Stateid.t -> unit) Hook.t + +(** User edits a sentence in the document *) +val document_edit_hook : (Stateid.t -> unit) Hook.t + +(** User requests evaluation of a sentence *) +val sentence_exec_hook : (Stateid.t -> unit) Hook.t + val get_doc : Feedback.doc_id -> doc val state_of_id : doc:doc -> diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index 7cecd801e4..aa16f9535d 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -188,11 +188,11 @@ let classify_vernac e = | VernacDeclareMLModule _ | VernacContext _ (* TASSI: unsure *) -> VtSideff [], VtNow | VernacProofMode pm -> VtProofMode pm, VtNow - | VernacInstance (_,((name,_),_,_),None,_) when not (Attributes.parse_drop_extra Attributes.program atts) -> + | VernacInstance ((name,_),_,_,None,_) when not (Attributes.parse_drop_extra Attributes.program atts) -> let polymorphic = Attributes.(parse_drop_extra polymorphic atts) in let guarantee = if polymorphic then Doesn'tGuaranteeOpacity else GuaranteesOpacity in VtStartProof (guarantee, idents_of_name name.CAst.v), VtLater - | VernacInstance (_,((name,_),_,_),_,_) -> + | VernacInstance ((name,_),_,_,_,_) -> VtSideff (idents_of_name name.CAst.v), VtLater (* Stm will install a new classifier to handle these *) | VernacBack _ | VernacAbortAll diff --git a/test-suite/success/Case18.v b/test-suite/success/Case18.v index be9ca8d41b..6bea435090 100644 --- a/test-suite/success/Case18.v +++ b/test-suite/success/Case18.v @@ -1,7 +1,10 @@ (* Check or-patterns *) +(* Non-interference with Numbers divisibility. *) +Reserved Notation "( p | q )" (at level 0). + Definition g x := - match x with ((((1 as x),_) | (_,x)), (_,(2 as y))|(y,_)) => (x,y) end. + match x with ((((1 as x),_) | (_,x)), ((_,(2 as y)) | (y,_))) => (x,y) end. Check (refl_equal _ : g ((1,2),(3,4)) = (1,3)). diff --git a/theories/Classes/CRelationClasses.v b/theories/Classes/CRelationClasses.v index c014ecc7ab..2dd254496b 100644 --- a/theories/Classes/CRelationClasses.v +++ b/theories/Classes/CRelationClasses.v @@ -337,7 +337,7 @@ Section Binary. morphism for equivalence (see Morphisms). It is also sufficient to show that [R] is antisymmetric w.r.t. [eqA] *) - Global Instance partial_order_antisym `(PartialOrder eqA R) : ! Antisymmetric A eqA R. + Global Instance partial_order_antisym `(PartialOrder eqA R) : Antisymmetric eqA R. Proof with auto. reduce_goal. apply H. firstorder. diff --git a/theories/Classes/EquivDec.v b/theories/Classes/EquivDec.v index e9a9d6aff2..7f26181108 100644 --- a/theories/Classes/EquivDec.v +++ b/theories/Classes/EquivDec.v @@ -94,7 +94,7 @@ Program Instance unit_eqdec : EqDec unit eq := fun x y => in_left. Obligation Tactic := unfold complement, equiv ; program_simpl. Program Instance prod_eqdec `(EqDec A eq, EqDec B eq) : - ! EqDec (prod A B) eq := + EqDec (prod A B) eq := { equiv_dec x y := let '(x1, x2) := x in let '(y1, y2) := y in @@ -115,7 +115,7 @@ Program Instance sum_eqdec `(EqDec A eq, EqDec B eq) : (** Objects of function spaces with countable domains like bool have decidable equality. Proving the reflection requires functional extensionality though. *) -Program Instance bool_function_eqdec `(EqDec A eq) : ! EqDec (bool -> A) eq := +Program Instance bool_function_eqdec `(EqDec A eq) : EqDec (bool -> A) eq := { equiv_dec f g := if f true == g true then if f false == g false then in_left @@ -130,7 +130,7 @@ Program Instance bool_function_eqdec `(EqDec A eq) : ! EqDec (bool -> A) eq := Require Import List. -Program Instance list_eqdec `(eqa : EqDec A eq) : ! EqDec (list A) eq := +Program Instance list_eqdec `(eqa : EqDec A eq) : EqDec (list A) eq := { equiv_dec := fix aux (x y : list A) := match x, y with diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v index 440b317573..3c0982cde7 100644 --- a/theories/Classes/RelationClasses.v +++ b/theories/Classes/RelationClasses.v @@ -464,7 +464,7 @@ Section Binary. morphism for equivalence (see Morphisms). It is also sufficient to show that [R] is antisymmetric w.r.t. [eqA] *) - Global Instance partial_order_antisym `(PartialOrder eqA R) : ! Antisymmetric A eqA R. + Global Instance partial_order_antisym `(PartialOrder eqA R) : Antisymmetric A eqA R. Proof with auto. reduce_goal. pose proof partial_order_equivalence as poe. do 3 red in poe. @@ -481,7 +481,7 @@ Hint Extern 3 (PartialOrder (flip _)) => class_apply PartialOrder_inverse : type (** The partial order defined by subrelation and relation equivalence. *) Program Instance subrelation_partial_order : - ! PartialOrder (relation A) relation_equivalence subrelation. + PartialOrder (@relation_equivalence A) subrelation. Next Obligation. Proof. diff --git a/toplevel/ccompile.ml b/toplevel/ccompile.ml index 2f63410761..7748134146 100644 --- a/toplevel/ccompile.ml +++ b/toplevel/ccompile.ml @@ -225,7 +225,7 @@ let do_vio opts copts = process happens outside of the STM *) if copts.vio_files <> [] || copts.vio_tasks <> [] then let iload_path = build_load_path opts in - List.iter Mltop.add_coq_path iload_path; + List.iter Loadpath.add_coq_path iload_path; (* Vio compile pass *) if copts.vio_files <> [] then schedule_vio copts; diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml index ec43dbb1d7..4ef31c73b7 100644 --- a/toplevel/coqargs.ml +++ b/toplevel/coqargs.ml @@ -46,8 +46,8 @@ type t = { load_rcfile : bool; rcfile : string option; - ml_includes : Mltop.coq_path list; - vo_includes : Mltop.coq_path list; + ml_includes : Loadpath.coq_path list; + vo_includes : Loadpath.coq_path list; vo_requires : (string * string option * bool option) list; (* None = No Import; Some false = Import; Some true = Export *) @@ -147,10 +147,10 @@ let default = { (* Functional arguments *) (******************************************************************************) let add_ml_include opts s = - Mltop.{ opts with ml_includes = {recursive = false; path_spec = MlPath s} :: opts.ml_includes } + Loadpath.{ opts with ml_includes = {recursive = false; path_spec = MlPath s} :: opts.ml_includes } let add_vo_include opts unix_path coq_path implicit = - let open Mltop in + let open Loadpath in let coq_path = Libnames.dirpath_of_string coq_path in { opts with vo_includes = { recursive = true; @@ -273,7 +273,7 @@ let usage help = end; let lp = Coqinit.toplevel_init_load_path () in (* Necessary for finding the toplevels below *) - List.iter Mltop.add_coq_path lp; + List.iter Loadpath.add_coq_path lp; help () (* Main parsing routine *) diff --git a/toplevel/coqargs.mli b/toplevel/coqargs.mli index d7f9819bee..015789c1f3 100644 --- a/toplevel/coqargs.mli +++ b/toplevel/coqargs.mli @@ -22,8 +22,8 @@ type t = { load_rcfile : bool; rcfile : string option; - ml_includes : Mltop.coq_path list; - vo_includes : Mltop.coq_path list; + ml_includes : Loadpath.coq_path list; + vo_includes : Loadpath.coq_path list; vo_requires : (string * string option * bool option) list; toplevel_name : Stm.interactive_top; @@ -69,4 +69,4 @@ val parse_args : help:(unit -> unit) -> init:t -> string list -> t * string list val exitcode : t -> int val require_libs : t -> (string * string option * bool option) list -val build_load_path : t -> Mltop.coq_path list +val build_load_path : t -> Loadpath.coq_path list diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index 74a089510e..cbe353004e 100644 --- a/toplevel/coqinit.ml +++ b/toplevel/coqinit.ml @@ -53,25 +53,25 @@ let load_rcfile ~rcfile ~state = (* Recursively puts dir in the LoadPath if -nois was not passed *) let build_stdlib_path ~load_init ~unix_path ~coq_path ~with_ml = - let open Mltop in + let open Loadpath in let add_ml = if with_ml then AddRecML else AddNoML in { recursive = true; path_spec = VoPath { unix_path; coq_path ; has_ml = add_ml; implicit = load_init } } let build_userlib_path ~unix_path = - let open Mltop in + let open Loadpath in { recursive = true; path_spec = VoPath { unix_path; coq_path = Libnames.default_root_prefix; - has_ml = Mltop.AddRecML; + has_ml = AddRecML; implicit = false; } } let ml_path_if c p = - let open Mltop in + let open Loadpath in let f x = { recursive = false; path_spec = MlPath x } in if c then List.map f p else [] @@ -85,7 +85,7 @@ let toplevel_init_load_path () = (* LoadPath for Coq user libraries *) let libs_init_load_path ~load_init = - let open Mltop in + let open Loadpath in let coqlib = Envars.coqlib () in let user_contrib = coqlib/"user-contrib" in let xdg_dirs = Envars.xdg_dirs ~warn:(fun x -> Feedback.msg_warning (str x)) in @@ -115,10 +115,10 @@ let libs_init_load_path ~load_init = (* Initialises the Ocaml toplevel before launching it, so that it can find the "include" file in the *source* directory *) let init_ocaml_path () = - let open Mltop in + let open Loadpath in let lp s = { recursive = false; path_spec = MlPath s } in let add_subdir dl = - Mltop.add_coq_path (lp (List.fold_left (/) Envars.coqroot [dl])) + Loadpath.add_coq_path (lp (List.fold_left (/) Envars.coqroot [dl])) in - Mltop.add_coq_path (lp (Envars.coqlib ())); + Loadpath.add_coq_path (lp (Envars.coqlib ())); List.iter add_subdir Coq_config.all_src_dirs diff --git a/toplevel/coqinit.mli b/toplevel/coqinit.mli index c891e736b4..04ec77a025 100644 --- a/toplevel/coqinit.mli +++ b/toplevel/coqinit.mli @@ -17,7 +17,7 @@ val load_rcfile : rcfile:(string option) -> state:Vernac.State.t -> Vernac.State val init_ocaml_path : unit -> unit (* LoadPath for toploop toplevels *) -val toplevel_init_load_path : unit -> Mltop.coq_path list +val toplevel_init_load_path : unit -> Loadpath.coq_path list (* LoadPath for Coq user libraries *) -val libs_init_load_path : load_init:bool -> Mltop.coq_path list +val libs_init_load_path : load_init:bool -> Loadpath.coq_path list diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index b769405cf6..460c2f126e 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -222,7 +222,7 @@ let init_toplevel ~help ~init custom_init arglist = exit 0; end; let top_lp = Coqinit.toplevel_init_load_path () in - List.iter Mltop.add_coq_path top_lp; + List.iter Loadpath.add_coq_path top_lp; let opts, extras = custom_init ~opts extras in Mltop.init_known_plugins (); diff --git a/user-contrib/Ltac2/Constr.v b/user-contrib/Ltac2/Constr.v index 1701bf4365..40946a8d56 100644 --- a/user-contrib/Ltac2/Constr.v +++ b/user-contrib/Ltac2/Constr.v @@ -48,7 +48,7 @@ Ltac2 @ external make : kind -> constr := "ltac2" "constr_make". Ltac2 @ external check : constr -> constr result := "ltac2" "constr_check". (** Checks that a constr generated by unsafe means is indeed safe in the current environment, and returns it, or the error otherwise. Panics if - not focussed. *) + not focused. *) Ltac2 @ external substnl : constr list -> int -> constr -> constr := "ltac2" "constr_substnl". (** [substnl [r₁;...;rₙ] k c] substitutes in parallel [Rel(k+1); ...; Rel(k+n)] with @@ -68,6 +68,6 @@ Ltac2 @ external constructor : inductive -> int -> constructor := "ltac2" "const End Unsafe. Ltac2 @ external in_context : ident -> constr -> (unit -> unit) -> constr := "ltac2" "constr_in_context". -(** On a focussed goal [Γ ⊢ A], [in_context id c tac] evaluates [tac] in a - focussed goal [Γ, id : c ⊢ ?X] and returns [fun (id : c) => t] where [t] is +(** On a focused goal [Γ ⊢ A], [in_context id c tac] evaluates [tac] in a + focused goal [Γ, id : c ⊢ ?X] and returns [fun (id : c) => t] where [t] is the proof built by the tactic. *) diff --git a/user-contrib/Ltac2/Pattern.v b/user-contrib/Ltac2/Pattern.v index 8d1fb0cd8a..5e8eef526e 100644 --- a/user-contrib/Ltac2/Pattern.v +++ b/user-contrib/Ltac2/Pattern.v @@ -25,7 +25,7 @@ Ltac2 @ external empty_context : unit -> context := Ltac2 @ external matches : t -> constr -> (ident * constr) list := "ltac2" "pattern_matches". (** If the term matches the pattern, returns the bound variables. If it doesn't, - fail with [Match_failure]. Panics if not focussed. *) + fail with [Match_failure]. Panics if not focused. *) Ltac2 @ external matches_subterm : t -> constr -> context * ((ident * constr) list) := "ltac2" "pattern_matches_subterm". diff --git a/vernac/classes.ml b/vernac/classes.ml index 5a7f60584a..ea66234993 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -494,21 +494,8 @@ let do_instance ~pstate env env' sigma ?hook ~tac ~global ~poly ~program_mode ct else CErrors.user_err Pp.(str "Unsolved obligations remaining.") in id, pstate -let interp_instance_context ~program_mode env ctx ?(generalize=false) pl bk cl = +let interp_instance_context ~program_mode env ctx ?(generalize=false) pl tclass = let sigma, decl = Constrexpr_ops.interp_univ_decl_opt env pl in - let tclass, ids = - match bk with - | Decl_kinds.Implicit -> - Implicit_quantifiers.implicit_application Id.Set.empty ~allow_partial:false - (fun avoid (clname, _) -> - match clname with - | Some cl -> - let t = CAst.make @@ CHole (None, Namegen.IntroAnonymous, None) in - t, avoid - | None -> failwith ("new instance: under-applied typeclass")) - cl - | Explicit -> cl, Id.Set.empty - in let tclass = if generalize then CAst.make @@ CGeneralization (Implicit, Some AbsPi, tclass) else tclass @@ -535,14 +522,13 @@ let interp_instance_context ~program_mode env ctx ?(generalize=false) pl bk cl = let sigma = resolve_typeclasses ~filter:Typeclasses.all_evars ~fail:true env sigma in sigma, cl, u, c', ctx', ctx, imps, args, decl - let new_instance ~pstate ?(global=false) ~program_mode - poly ctx (instid, bk, cl) props + poly instid ctx cl props ?(generalize=true) ?(tac:unit Proofview.tactic option) ?hook pri = let env = Global.env() in let ({CAst.loc;v=instid}, pl) = instid in let sigma, k, u, cty, ctx', ctx, imps, subst, decl = - interp_instance_context ~program_mode env ~generalize ctx pl bk cl + interp_instance_context ~program_mode env ~generalize ctx pl cl in let id = match instid with @@ -555,10 +541,10 @@ let new_instance ~pstate ?(global=false) ~program_mode do_instance ~pstate env env' sigma ?hook ~tac ~global ~poly ~program_mode cty k u ctx ctx' pri decl imps subst id props -let declare_new_instance ?(global=false) ~program_mode poly ctx (instid, bk, cl) pri = +let declare_new_instance ?(global=false) ~program_mode poly instid ctx cl pri = let env = Global.env() in let ({CAst.loc;v=instid}, pl) = instid in let sigma, k, u, cty, ctx', ctx, imps, subst, decl = - interp_instance_context ~program_mode env ctx pl bk cl + interp_instance_context ~program_mode env ctx pl cl in do_declare_instance env sigma ~global ~poly k u ctx ctx' pri decl imps subst instid diff --git a/vernac/classes.mli b/vernac/classes.mli index 57bb9ce312..8d5f3e3a06 100644 --- a/vernac/classes.mli +++ b/vernac/classes.mli @@ -46,28 +46,29 @@ val declare_instance_constant : unit val new_instance : - pstate:Proof_global.t option -> - ?global:bool (** Not global by default. *) -> - program_mode:bool -> - Decl_kinds.polymorphic -> - local_binder_expr list -> - Vernacexpr.typeclass_constraint -> - (bool * constr_expr) option -> - ?generalize:bool -> - ?tac:unit Proofview.tactic -> - ?hook:(GlobRef.t -> unit) -> - Hints.hint_info_expr -> - (* May open a proof *) - Id.t * Proof_global.t option - -val declare_new_instance : - ?global:bool (** Not global by default. *) -> - program_mode:bool -> - Decl_kinds.polymorphic -> - local_binder_expr list -> - ident_decl * Decl_kinds.binding_kind * constr_expr -> - Hints.hint_info_expr -> - unit + pstate:Proof_global.t option + -> ?global:bool (** Not global by default. *) + -> program_mode:bool + -> Decl_kinds.polymorphic + -> name_decl + -> local_binder_expr list + -> constr_expr + -> (bool * constr_expr) option + -> ?generalize:bool + -> ?tac:unit Proofview.tactic + -> ?hook:(GlobRef.t -> unit) + -> Hints.hint_info_expr + -> Id.t * Proof_global.t option (* May open a proof *) + +val declare_new_instance + : ?global:bool (** Not global by default. *) + -> program_mode:bool + -> Decl_kinds.polymorphic + -> ident_decl + -> local_binder_expr list + -> constr_expr + -> Hints.hint_info_expr + -> unit (** {6 Low level interface used by Add Morphism, do not use } *) val mk_instance : typeclass -> hint_info -> bool -> GlobRef.t -> instance diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml index 568e5b9997..9bc225475d 100644 --- a/vernac/egramcoq.ml +++ b/vernac/egramcoq.ml @@ -546,6 +546,15 @@ let extend_constr state forpat ng = let constr_levels = GramState.field () +let is_disjunctive_pattern_rule ng = + String.is_sub "( _ | " (snd ng.notgram_notation) 0 + +let warn_disj_pattern_notation = + let open Pp in + let pp ng = str "Use of " ++ Notation.pr_notation ng.notgram_notation ++ + str " Notation is deprecated as it is inconsistent with pattern syntax." in + CWarnings.create ~name:"disj-pattern-notation" ~category:"notation" ~default:CWarnings.Disabled pp + let extend_constr_notation ng state = let levels = match GramState.get state constr_levels with | None -> String.Map.add "constr" default_constr_levels String.Map.empty @@ -553,8 +562,13 @@ let extend_constr_notation ng state = in (* Add the notation in constr *) let (r, levels) = extend_constr levels ForConstr ng in - (* Add the notation in cases_pattern *) - let (r', levels) = extend_constr levels ForPattern ng in + (* Add the notation in cases_pattern, unless it would disrupt *) + (* parsing nested disjunctive patterns. *) + let (r', levels) = + if is_disjunctive_pattern_rule ng then begin + warn_disj_pattern_notation ng; + ([], levels) + end else extend_constr levels ForPattern ng in let state = GramState.set state constr_levels levels in (r @ r', state) diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index 6438b48e32..7c8c2b10ab 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -303,7 +303,7 @@ GRAMMAR EXTEND Gram [ [ "@{" ; l = LIST0 identref; ext = [ "+" -> { true } | -> { false } ]; cs = [ "|"; l' = LIST0 univ_constraint SEP ","; ext = [ "+" -> { true } | -> { false } ]; "}" -> { (l',ext) } - | ext = [ "}" -> { true } | "|}" -> { false } ] -> { ([], ext) } ] + | ext = [ "}" -> { true } | bar_cbrace -> { false } ] -> { ([], ext) } ] -> { let open UState in { univdecl_instance = l; @@ -723,11 +723,11 @@ GRAMMAR EXTEND Gram { VernacContext (List.flatten c) } | IDENT "Instance"; namesup = instance_name; ":"; - expl = [ "!" -> { Decl_kinds.Implicit } | -> { Decl_kinds.Explicit } ] ; t = operconstr LEVEL "200"; + t = operconstr LEVEL "200"; info = hint_info ; props = [ ":="; "{"; r = record_declaration; "}" -> { Some (true,r) } | ":="; c = lconstr -> { Some (false,c) } | -> { None } ] -> - { VernacInstance (snd namesup,(fst namesup,expl,t),props,info) } + { VernacInstance (fst namesup,snd namesup,t,props,info) } | IDENT "Existing"; IDENT "Instance"; id = global; info = hint_info -> @@ -888,9 +888,9 @@ GRAMMAR EXTEND Gram (* Hack! Should be in grammar_ext, but camlp5 factorizes badly *) | IDENT "Declare"; IDENT "Instance"; id = ident_decl; bl = binders; ":"; - expl = [ "!" -> { Decl_kinds.Implicit } | -> { Decl_kinds.Explicit } ] ; t = operconstr LEVEL "200"; + t = operconstr LEVEL "200"; info = hint_info -> - { VernacDeclareInstance (bl, (id, expl, t), info) } + { VernacDeclareInstance (id, bl, t, info) } (* Should be in syntax, but camlp5 would not factorize *) | IDENT "Declare"; IDENT "Scope"; sc = IDENT -> diff --git a/vernac/loadpath.ml b/vernac/loadpath.ml new file mode 100644 index 0000000000..1bb44d0ef1 --- /dev/null +++ b/vernac/loadpath.ml @@ -0,0 +1,273 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +open Util +module DP = Names.DirPath + +(** Load paths. Mapping from physical to logical paths. *) + +type t = { + path_physical : CUnix.physical_path; + path_logical : DP.t; + path_implicit : bool; +} + +let load_paths = Summary.ref ([] : t list) ~name:"LOADPATHS" + +let logical p = p.path_logical +let physical p = p.path_physical + +let pp p = + let dir = DP.print p.path_logical in + let path = Pp.str (CUnix.escaped_string_of_physical_path p.path_physical) in + Pp.(hov 2 (dir ++ spc () ++ path)) + +let get_load_paths () = !load_paths + +let anomaly_too_many_paths path = + CErrors.anomaly Pp.(str "Several logical paths are associated to" ++ spc () ++ str path ++ str ".") + +let find_load_path phys_dir = + let phys_dir = CUnix.canonical_path_name phys_dir in + let filter p = String.equal p.path_physical phys_dir in + let paths = List.filter filter !load_paths in + match paths with + | [] -> raise Not_found + | [p] -> p + | _ -> anomaly_too_many_paths phys_dir + +let remove_load_path dir = + let filter p = not (String.equal p.path_physical dir) in + load_paths := List.filter filter !load_paths + +let warn_overriding_logical_loadpath = + CWarnings.create ~name:"overriding-logical-loadpath" ~category:"loadpath" + (fun (phys_path, old_path, coq_path) -> + Pp.(seq [str phys_path; strbrk " was previously bound to " + ; DP.print old_path; strbrk "; it is remapped to " + ; DP.print coq_path])) + +let add_load_path phys_path coq_path ~implicit = + let phys_path = CUnix.canonical_path_name phys_path in + let filter p = String.equal p.path_physical phys_path in + let binding = { + path_logical = coq_path; + path_physical = phys_path; + path_implicit = implicit; + } in + match List.filter filter !load_paths with + | [] -> + load_paths := binding :: !load_paths + | [{ path_logical = old_path; path_implicit = old_implicit }] -> + let replace = + if DP.equal coq_path old_path then + implicit <> old_implicit + else + let () = + (* Do not warn when overriding the default "-I ." path *) + if not (DP.equal old_path Libnames.default_root_prefix) then + warn_overriding_logical_loadpath (phys_path, old_path, coq_path) + in + true in + if replace then + begin + remove_load_path phys_path; + load_paths := binding :: !load_paths; + end + | _ -> anomaly_too_many_paths phys_path + +let filter_path f = + let rec aux = function + | [] -> [] + | p :: l -> + if f p.path_logical then (p.path_physical, p.path_logical) :: aux l + else aux l + in + aux !load_paths + +let expand_path ?root dir = + let rec aux = function + | [] -> [] + | { path_physical = ph; path_logical = lg; path_implicit = implicit } :: l -> + let success = + match root with + | None -> + if implicit then Libnames.is_dirpath_suffix_of dir lg + else DP.equal dir lg + | Some root -> + Libnames.(is_dirpath_prefix_of root lg && + is_dirpath_suffix_of dir (drop_dirpath_prefix root lg)) in + if success then (ph, lg) :: aux l else aux l in + aux !load_paths + +let locate_file fname = + let paths = List.map physical !load_paths in + let _,longfname = + System.find_file_in_path ~warn:(not !Flags.quiet) paths fname in + longfname + +(************************************************************************) +(*s Locate absolute or partially qualified library names in the path *) + +type library_location = LibLoaded | LibInPath +type locate_error = LibUnmappedDir | LibNotFound +type 'a locate_result = ('a, locate_error) result + +let warn_several_object_files = + CWarnings.create ~name:"several-object-files" ~category:"require" + Pp.(fun (vi, vo) -> + seq [ str "Loading"; spc (); str vi + ; strbrk " instead of "; str vo + ; strbrk " because it is more recent" + ]) + + +let select_vo_file ~warn loadpath base = + let find ext = + let loadpath = List.map fst loadpath in + try + let name = Names.Id.to_string base ^ ext in + let lpath, file = + System.where_in_path ~warn loadpath name in + Some (lpath, file) + with Not_found -> None in + match find ".vo", find ".vio" with + | None, None -> + Error LibNotFound + | Some res, None | None, Some res -> + Ok res + | Some (_, vo), Some (_, vi as resvi) + when Unix.((stat vo).st_mtime < (stat vi).st_mtime) -> + warn_several_object_files (vi, vo); + Ok resvi + | Some resvo, Some _ -> + Ok resvo + +let locate_absolute_library dir : CUnix.physical_path locate_result = + (* Search in loadpath *) + let pref, base = Libnames.split_dirpath dir in + let loadpath = filter_path (fun dir -> DP.equal dir pref) in + match loadpath with + | [] -> Error LibUnmappedDir + | _ -> + match select_vo_file ~warn:false loadpath base with + | Ok (_, file) -> Ok file + | Error fail -> Error fail + +let locate_qualified_library ?root ?(warn = true) qid : + (library_location * DP.t * CUnix.physical_path) locate_result = + (* Search library in loadpath *) + let dir, base = Libnames.repr_qualid qid in + let loadpath = expand_path ?root dir in + match loadpath with + | [] -> Error LibUnmappedDir + | _ -> + match select_vo_file ~warn loadpath base with + | Ok (lpath, file) -> + let dir = Libnames.add_dirpath_suffix + (CString.List.assoc lpath loadpath) base in + (* Look if loaded *) + if Library.library_is_loaded dir + then Ok (LibLoaded, dir, Library.library_full_filename dir) + (* Otherwise, look for it in the file system *) + else Ok (LibInPath, dir, file) + | Error fail -> Error fail + +let error_unmapped_dir qid = + let prefix, _ = Libnames.repr_qualid qid in + CErrors.user_err ~hdr:"load_absolute_library_from" + Pp.(seq [ str "Cannot load "; Libnames.pr_qualid qid; str ":"; spc () + ; str "no physical path bound to"; spc () + ; DP.print prefix; fnl () + ]) + +let error_lib_not_found qid = + CErrors.user_err ~hdr:"load_absolute_library_from" + Pp.(seq [ str "Cannot find library "; Libnames.pr_qualid qid; str" in loadpath"]) + +let try_locate_absolute_library dir = + match locate_absolute_library dir with + | Ok res -> res + | Error LibUnmappedDir -> + error_unmapped_dir (Libnames.qualid_of_dirpath dir) + | Error LibNotFound -> + error_lib_not_found (Libnames.qualid_of_dirpath dir) + +(** { 5 Extending the load path } *) + +(* Adds a path to the Coq and ML paths *) +type add_ml = AddNoML | AddTopML | AddRecML + +type vo_path_spec = { + unix_path : string; (* Filesystem path contaning vo/ml files *) + coq_path : DP.t; (* Coq prefix for the path *) + implicit : bool; (* [implicit = true] avoids having to qualify with [coq_path] *) + has_ml : add_ml; (* If [has_ml] is true, the directory will also be search for plugins *) +} + +type coq_path_spec = + | VoPath of vo_path_spec + | MlPath of string + +type coq_path = { + path_spec: coq_path_spec; + recursive: bool; +} + +let warn_cannot_open_path = + CWarnings.create ~name:"cannot-open-path" ~category:"filesystem" + (fun unix_path -> Pp.(str "Cannot open " ++ str unix_path)) + +let warn_cannot_use_directory = + CWarnings.create ~name:"cannot-use-directory" ~category:"filesystem" + (fun d -> + Pp.(str "Directory " ++ str d ++ + strbrk " cannot be used as a Coq identifier (skipped)")) + +let convert_string d = + try Names.Id.of_string d + with + | CErrors.UserError _ -> + let d = Unicode.escaped_if_non_utf8 d in + warn_cannot_use_directory d; + raise Exit + +let add_vo_path ~recursive lp = + let unix_path = lp.unix_path in + let implicit = lp.implicit in + if System.exists_dir unix_path then + let dirs = if recursive then System.all_subdirs ~unix_path else [] in + let prefix = DP.repr lp.coq_path in + let convert_dirs (lp, cp) = + try + let path = List.rev_map convert_string cp @ prefix in + Some (lp, DP.make path) + with Exit -> None + in + let dirs = List.map_filter convert_dirs dirs in + let add_ml_dir = Mltop.add_ml_dir ~recursive:false in + let () = match lp.has_ml with + | AddNoML -> () + | AddTopML -> + Mltop.add_ml_dir ~recursive:false unix_path + | AddRecML -> + List.iter (fun (lp,_) -> add_ml_dir lp) dirs; + add_ml_dir unix_path in + let add (path, dir) = add_load_path path ~implicit dir in + let () = List.iter add dirs in + add_load_path unix_path ~implicit lp.coq_path + else + warn_cannot_open_path unix_path + +let add_coq_path { recursive; path_spec } = match path_spec with + | VoPath lp -> + add_vo_path ~recursive lp + | MlPath dir -> + Mltop.add_ml_dir ~recursive dir diff --git a/library/loadpath.mli b/vernac/loadpath.mli index 4044ca1127..d393fc35b5 100644 --- a/library/loadpath.mli +++ b/vernac/loadpath.mli @@ -20,19 +20,15 @@ open Names type t (** Type of loadpath bindings. *) -val physical : t -> CUnix.physical_path -(** Get the physical path (filesystem location) of a loadpath. *) - val logical : t -> DirPath.t (** Get the logical path (Coq module hierarchy) of a loadpath. *) +val pp : t -> Pp.t +(** Print a load path *) + val get_load_paths : unit -> t list (** Get the current loadpath association. *) -val add_load_path : CUnix.physical_path -> DirPath.t -> implicit:bool -> unit -(** [add_load_path phys log type] adds the binding [phys := log] to the current - loadpaths. *) - val remove_load_path : CUnix.physical_path -> unit (** Remove the current logical path binding associated to a given physical path, if any. *) @@ -41,17 +37,53 @@ val find_load_path : CUnix.physical_path -> t (** Get the binding associated to a physical path. Raises [Not_found] if there is none. *) -val is_in_load_paths : CUnix.physical_path -> bool -(** Whether a physical path is currently bound. *) - -val expand_path : ?root:DirPath.t -> DirPath.t -> (CUnix.physical_path * DirPath.t) list -(** Given a relative logical path, associate the list of absolute physical and - logical paths which are possible matches of it. *) - -val filter_path : (DirPath.t -> bool) -> (CUnix.physical_path * DirPath.t) list -(** As {!expand_path} but uses a filter function instead, and ignores the - implicit status of loadpaths. *) - val locate_file : string -> string (** Locate a file among the registered paths. Do not use this function, as it does not respect the visibility of paths. *) + +(** {6 Locate a library in the load path } *) +type library_location = LibLoaded | LibInPath +type locate_error = LibUnmappedDir | LibNotFound +type 'a locate_result = ('a, locate_error) result + +val locate_qualified_library + : ?root:DirPath.t + -> ?warn:bool + -> Libnames.qualid + -> (library_location * DirPath.t * CUnix.physical_path) locate_result + +(** Locates a library by implicit name. + + @raise LibUnmappedDir if the library is not in the path + @raise LibNotFound if there is no corresponding file in the path + +*) + +val try_locate_absolute_library : DirPath.t -> string + +(** {6 Extending the Load Path } *) + +(** Adds a path to the Coq and ML paths *) +type add_ml = AddNoML | AddTopML | AddRecML + +type vo_path_spec = { + unix_path : string; + (** Filesystem path contaning vo/ml files *) + coq_path : Names.DirPath.t; + (** Coq prefix for the path *) + implicit : bool; + (** [implicit = true] avoids having to qualify with [coq_path] *) + has_ml : add_ml; + (** If [has_ml] is true, the directory will also be search for plugins *) +} + +type coq_path_spec = + | VoPath of vo_path_spec + | MlPath of string + +type coq_path = { + path_spec: coq_path_spec; + recursive: bool; +} + +val add_coq_path : coq_path -> unit diff --git a/vernac/mltop.ml b/vernac/mltop.ml index 78e26c65d4..bbee9988d0 100644 --- a/vernac/mltop.ml +++ b/vernac/mltop.ml @@ -159,75 +159,9 @@ let add_ml_dir s = | _ -> () (* For Rec Add ML Path (-R) *) -let add_rec_ml_dir unix_path = - List.iter (fun (lp,_) -> add_ml_dir lp) (all_subdirs ~unix_path) - -(* Adding files to Coq and ML loadpath *) - -let warn_cannot_use_directory = - CWarnings.create ~name:"cannot-use-directory" ~category:"filesystem" - (fun d -> - str "Directory " ++ str d ++ - strbrk " cannot be used as a Coq identifier (skipped)") - -let convert_string d = - try Names.Id.of_string d - with UserError _ -> - let d = Unicode.escaped_if_non_utf8 d in - warn_cannot_use_directory d; - raise Exit - -let warn_cannot_open_path = - CWarnings.create ~name:"cannot-open-path" ~category:"filesystem" - (fun unix_path -> str "Cannot open " ++ str unix_path) - -type add_ml = AddNoML | AddTopML | AddRecML - -type vo_path_spec = { - unix_path : string; - coq_path : Names.DirPath.t; - implicit : bool; - has_ml : add_ml; -} - -type coq_path_spec = - | VoPath of vo_path_spec - | MlPath of string - -type coq_path = { - path_spec: coq_path_spec; - recursive: bool; -} - -let add_vo_path ~recursive lp = - let unix_path = lp.unix_path in - let implicit = lp.implicit in - if exists_dir unix_path then - let dirs = if recursive then all_subdirs ~unix_path else [] in - let prefix = Names.DirPath.repr lp.coq_path in - let convert_dirs (lp, cp) = - try - let path = List.rev_map convert_string cp @ prefix in - Some (lp, Names.DirPath.make path) - with Exit -> None - in - let dirs = List.map_filter convert_dirs dirs in - let () = match lp.has_ml with - | AddNoML -> () - | AddTopML -> add_ml_dir unix_path - | AddRecML -> List.iter (fun (lp,_) -> add_ml_dir lp) dirs; add_ml_dir unix_path in - let add (path, dir) = - Loadpath.add_load_path path ~implicit dir in - let () = List.iter add dirs in - Loadpath.add_load_path unix_path ~implicit lp.coq_path - else - warn_cannot_open_path unix_path - -let add_coq_path { recursive; path_spec } = match path_spec with - | VoPath lp -> - add_vo_path ~recursive lp - | MlPath dir -> - if recursive then add_rec_ml_dir dir else add_ml_dir dir +let add_ml_dir ~recursive unix_path = + let dirs = if recursive then (all_subdirs ~unix_path) else [unix_path,[]] in + List.iter (fun (lp,_) -> add_ml_dir lp) dirs (* convertit un nom quelconque en nom de fichier ou de module *) let mod_of_name name = diff --git a/vernac/mltop.mli b/vernac/mltop.mli index 3d796aa4aa..b457c9c88f 100644 --- a/vernac/mltop.mli +++ b/vernac/mltop.mli @@ -32,6 +32,9 @@ val ocaml_toploop : unit -> unit (** {5 ML Dynlink} *) +(** Adds a dir to the plugin search path *) +val add_ml_dir : recursive:bool -> string -> unit + (** Tests if we can load ML files *) val has_dynlink : bool @@ -41,27 +44,6 @@ val dir_ml_load : string -> unit (** Dynamic interpretation of .ml *) val dir_ml_use : string -> unit -(** Adds a path to the Coq and ML paths *) -type add_ml = AddNoML | AddTopML | AddRecML - -type vo_path_spec = { - unix_path : string; (* Filesystem path contaning vo/ml files *) - coq_path : Names.DirPath.t; (* Coq prefix for the path *) - implicit : bool; (* [implicit = true] avoids having to qualify with [coq_path] *) - has_ml : add_ml; (* If [has_ml] is true, the directory will also be search for plugins *) -} - -type coq_path_spec = - | VoPath of vo_path_spec - | MlPath of string - -type coq_path = { - path_spec: coq_path_spec; - recursive: bool; -} - -val add_coq_path : coq_path -> unit - (** List of modules linked to the toplevel *) val add_known_module : string -> unit val module_is_known : string -> bool diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index f2332bab8b..2e97a169cc 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -911,7 +911,7 @@ open Pputils spc() ++ pr_class_rawexpr c2) ) - | VernacInstance (sup, (instid, bk, cl), props, info) -> + | VernacInstance (instid, sup, cl, props, info) -> return ( hov 1 ( keyword "Instance" ++ @@ -920,7 +920,6 @@ open Pputils | { v = Anonymous }, _ -> mt ()) ++ pr_and_type_binders_arg sup ++ str":" ++ spc () ++ - (match bk with Implicit -> str "! " | Explicit -> mt ()) ++ pr_constr env sigma cl ++ pr_hint_info (pr_constr_pattern_expr env sigma) info ++ (match props with | Some (true, { v = CRecord l}) -> spc () ++ str":=" ++ spc () ++ str"{" ++ pr_record_body l ++ str "}" @@ -929,13 +928,12 @@ open Pputils | None -> mt())) ) - | VernacDeclareInstance (sup, (instid, bk, cl), info) -> + | VernacDeclareInstance (instid, sup, cl, info) -> return ( hov 1 ( keyword "Declare Instance" ++ spc () ++ pr_ident_decl instid ++ spc () ++ pr_and_type_binders_arg sup ++ str":" ++ spc () ++ - (match bk with Implicit -> str "! " | Explicit -> mt ()) ++ pr_constr env sigma cl ++ pr_hint_info (pr_constr_pattern_expr env sigma) info) ) diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib index 7f5c265eea..57c56a58f9 100644 --- a/vernac/vernac.mllib +++ b/vernac/vernac.mllib @@ -32,6 +32,7 @@ Assumptions Vernacstate Mltop Topfmt +Loadpath Vernacentries Misctypes diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 918852239a..b9d1326ba5 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -201,11 +201,6 @@ let show_match id = (* "Print" commands *) -let print_path_entry p = - let dir = DirPath.print (Loadpath.logical p) in - let path = str (CUnix.escaped_string_of_physical_path (Loadpath.physical p)) in - Pp.hov 2 (dir ++ spc () ++ path) - let print_loadpath dir = let l = Loadpath.get_load_paths () in let l = match dir with @@ -215,7 +210,7 @@ let print_loadpath dir = List.filter filter l in str "Logical Path / Physical path:" ++ fnl () ++ - prlist_with_sep fnl print_path_entry l + prlist_with_sep fnl Loadpath.pp l let print_modules () = let opened = Library.opened_libraries () @@ -444,9 +439,9 @@ let locate_file f = str file let msg_found_library = function - | Library.LibLoaded, fulldir, file -> + | Loadpath.LibLoaded, fulldir, file -> hov 0 (DirPath.print fulldir ++ strbrk " has been loaded from file " ++ str file) - | Library.LibInPath, fulldir, file -> + | Loadpath.LibInPath, fulldir, file -> hov 0 (DirPath.print fulldir ++ strbrk " is bound to file " ++ str file) let err_unmapped_library ?from qid = @@ -471,10 +466,11 @@ let err_notfound_library ?from qid = (strbrk "Unable to locate library " ++ pr_qualid qid ++ prefix) let print_located_library qid = - try msg_found_library (Library.locate_qualified_library ~warn:false qid) - with - | Library.LibUnmappedDir -> err_unmapped_library qid - | Library.LibNotFound -> err_notfound_library qid + let open Loadpath in + match locate_qualified_library ~warn:false qid with + | Ok lib -> msg_found_library lib + | Error LibUnmappedDir -> err_unmapped_library qid + | Error LibNotFound -> err_notfound_library qid let smart_global r = let gr = Smartlocate.smart_global r in @@ -1026,18 +1022,18 @@ let vernac_require from import qidl = Some (Libnames.add_dirpath_suffix hd tl) in let locate qid = - try - let warn = not !Flags.quiet in - let (_, dir, f) = Library.locate_qualified_library ?root ~warn qid in - (dir, f) - with - | Library.LibUnmappedDir -> err_unmapped_library ?from:root qid - | Library.LibNotFound -> err_notfound_library ?from:root qid + let open Loadpath in + let warn = not !Flags.quiet in + match locate_qualified_library ?root ~warn qid with + | Ok (_,dir,f) -> dir, f + | Error LibUnmappedDir -> err_unmapped_library ?from:root qid + | Error LibNotFound -> err_notfound_library ?from:root qid in let modrefl = List.map locate qidl in if Dumpglob.dump () then List.iter2 (fun {CAst.loc} dp -> Dumpglob.dump_libref ?loc dp "lib") qidl (List.map fst modrefl); - Library.require_library_from_dirpath modrefl import + let lib_resolver = Loadpath.try_locate_absolute_library in + Library.require_library_from_dirpath ~lib_resolver modrefl import (* Coercions and canonical structures *) @@ -1062,18 +1058,18 @@ let vernac_identity_coercion ~atts id qids qidt = (* Type classes *) -let vernac_instance ~atts sup inst props pri = +let vernac_instance ~atts name bl t props pri = let open DefAttributes in let global = not (make_section_locality atts.locality) in - Dumpglob.dump_constraint (fst (pi1 inst)) false "inst"; + Dumpglob.dump_constraint (fst name) false "inst"; let program_mode = atts.program in - Classes.new_instance ~program_mode ~global atts.polymorphic sup inst props pri + Classes.new_instance ~program_mode ~global atts.polymorphic name bl t props pri -let vernac_declare_instance ~atts sup inst pri = +let vernac_declare_instance ~atts id bl inst pri = let open DefAttributes in let global = not (make_section_locality atts.locality) in - Dumpglob.dump_definition (fst (pi1 inst)) false "inst"; - Classes.declare_new_instance ~program_mode:atts.program ~global atts.polymorphic sup inst pri + Dumpglob.dump_definition (fst id) false "inst"; + Classes.declare_new_instance ~program_mode:atts.program ~global atts.polymorphic id bl inst pri let vernac_context ~poly l = if not (ComAssumption.context poly l) then Feedback.feedback Feedback.AddedAxiom @@ -1133,7 +1129,7 @@ let expand filename = Envars.expand_path_macros ~warn:(fun x -> Feedback.msg_warning (str x)) filename let vernac_add_loadpath implicit pdir ldiropt = - let open Mltop in + let open Loadpath in let pdir = expand pdir in let alias = Option.default Libnames.default_root_prefix ldiropt in add_coq_path { recursive = true; @@ -1141,11 +1137,10 @@ let vernac_add_loadpath implicit pdir ldiropt = let vernac_remove_loadpath path = Loadpath.remove_load_path (expand path) - (* Coq syntax for ML or system commands *) let vernac_add_ml_path isrec path = - let open Mltop in + let open Loadpath in add_coq_path { recursive = isrec; path_spec = MlPath (expand path) } let vernac_declare_ml_module ~local l = @@ -2204,7 +2199,7 @@ let with_fail ~st f = try let _ = f () in raise HasNotFailed with | HasNotFailed as e -> raise e - | e -> + | e when CErrors.noncritical e || e = Timeout -> let e = CErrors.push e in raise (HasFailed (CErrors.iprint (ExplainErr.process_vernac_interp_error ~allow_uncaught:false e))) @@ -2377,10 +2372,10 @@ let rec interp_expr ?proof ~atts ~st c : Proof_global.t option = pstate (* Type classes *) - | VernacInstance (sup, inst, props, info) -> - snd @@ with_def_attributes ~atts (vernac_instance ~pstate sup inst props info) - | VernacDeclareInstance (sup, inst, info) -> - with_def_attributes ~atts vernac_declare_instance sup inst info; + | VernacInstance (name, bl, t, props, info) -> + snd @@ with_def_attributes ~atts (vernac_instance ~pstate name bl t props info) + | VernacDeclareInstance (id, bl, inst, info) -> + with_def_attributes ~atts vernac_declare_instance id bl inst info; pstate | VernacContext sup -> let () = vernac_context ~poly:(only_polymorphism atts) sup in diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index 23633e39ab..f946e0596e 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -303,15 +303,17 @@ type nonrec vernac_expr = (* Type classes *) | VernacInstance of - local_binder_expr list * (* super *) - typeclass_constraint * (* instance name, class name, params *) - (bool * constr_expr) option * (* props *) - Hints.hint_info_expr + name_decl * (* name *) + local_binder_expr list * (* binders *) + constr_expr * (* type *) + (bool * constr_expr) option * (* body (bool=true when using {}) *) + Hints.hint_info_expr | VernacDeclareInstance of - local_binder_expr list * (* super *) - (ident_decl * Decl_kinds.binding_kind * constr_expr) * (* instance name, class name, params *) - Hints.hint_info_expr + ident_decl * (* name *) + local_binder_expr list * (* binders *) + constr_expr * (* type *) + Hints.hint_info_expr | VernacContext of local_binder_expr list |