diff options
Diffstat (limited to 'doc')
56 files changed, 1166 insertions, 633 deletions
diff --git a/doc/LICENSE b/doc/LICENSE index 3789d91040..9f3a6b3f4c 100644 --- a/doc/LICENSE +++ b/doc/LICENSE @@ -2,25 +2,25 @@ The Coq Reference Manual is a collective work from the Coq Development Team whose members are listed in the file CREDITS of the Coq source package. All related documents (the LaTeX and BibTeX sources, the embedded png files, and the PostScript, PDF and html outputs) are -copyright (c) INRIA 1999-2018, with the exception of the Ubuntu font -file UbuntuMono-B.ttf, which is -Copyright 2010,2011 Canonical Ltd and licensed under the Ubuntu font -license, version 1.0 -(https://www.ubuntu.com/legal/terms-and-policies/font-licence), and its -derivative CoqNotations.ttf distributed under the same license. The -material connected to the Reference Manual may be distributed only -subject to the terms and conditions set forth in the Open Publication -License, v1.0 or later (the latest version is presently available at -http://www.opencontent.org/openpub/). Options A and B are *not* -elected. +copyright (c) 1999-2019, Inria, CNRS and contributors, with the +exception of the Ubuntu font file UbuntuMono-B.ttf, which is Copyright +2010,2011 Canonical Ltd and licensed under the Ubuntu font license, +version 1.0 +(https://www.ubuntu.com/legal/terms-and-policies/font-licence), and +its derivative CoqNotations.ttf distributed under the same +license. The material connected to the Reference Manual may be +distributed only subject to the terms and conditions set forth in the +Open Publication License, v1.0 or later (the latest version is +presently available at http://www.opencontent.org/openpub/). Options +A and B are *not* elected. The Coq Standard Library is a collective work from the Coq Development Team whose members are listed in the file CREDITS of the Coq source package. All related documents (the Coq vernacular source files and -the PostScript, PDF and html outputs) are copyright (c) INRIA -1999-2018. The material connected to the Standard Library is -distributed under the terms of the Lesser General Public License -version 2.1 or later. +the PostScript, PDF and html outputs) are copyright (c) 1999-2019, +Inria, CNRS and contributors. The material connected to the Standard +Library is distributed under the terms of the Lesser General Public +License version 2.1 or later. ---------------------------------------------------------------------- diff --git a/doc/changelog/03-notations/10180-deprecate-notations.rst b/doc/changelog/03-notations/10180-deprecate-notations.rst new file mode 100644 index 0000000000..01f2e893ed --- /dev/null +++ b/doc/changelog/03-notations/10180-deprecate-notations.rst @@ -0,0 +1,6 @@ +- The :cmd:`Notation` and :cmd:`Infix` commands now support the `deprecated` + attribute. The former `compat` annotation for notations is + deprecated, and its semantics changed. It is now made equivalent to using + a `deprecated` attribute, and is no longer connected with the `-compat` + command-line flag. + (`#10180 <https://github.com/coq/coq/pull/10180>`_, by Maxime Dénès). diff --git a/doc/changelog/04-tactics/10205-discriminate-HoTT.rst b/doc/changelog/04-tactics/10205-discriminate-HoTT.rst deleted file mode 100644 index bb2d2a092e..0000000000 --- a/doc/changelog/04-tactics/10205-discriminate-HoTT.rst +++ /dev/null @@ -1,6 +0,0 @@ -- Make the :tacn:`discriminate` tactic work together with - :flag:`Universe Polymorphism` and equality in :g:`Type`. This, - in particular, makes :tacn:`discriminate` compatible with the HoTT - library https://github.com/HoTT/HoTT. - (`#10205 <https://github.com/coq/coq/pull/10205>`_, - by Andreas Lynge, review by Pierre-Marie Pédrot and Matthieu Sozeau) diff --git a/doc/changelog/07-commands-and-options/10336-ambiguous-paths.rst b/doc/changelog/07-commands-and-options/10336-ambiguous-paths.rst new file mode 100644 index 0000000000..151c400b2c --- /dev/null +++ b/doc/changelog/07-commands-and-options/10336-ambiguous-paths.rst @@ -0,0 +1,5 @@ +- Improve the ambiguous paths warning to indicate which path is ambiguous with + new one + (`#10336 <https://github.com/coq/coq/pull/10336>`_, + closes `#3219 <https://github.com/coq/coq/issues/3219>`_, + by Kazuhiko Sakaguchi). diff --git a/doc/changelog/12-misc/10019-PG-proof-diffs.rst b/doc/changelog/12-misc/10019-PG-proof-diffs.rst deleted file mode 100644 index b2d191be26..0000000000 --- a/doc/changelog/12-misc/10019-PG-proof-diffs.rst +++ /dev/null @@ -1,3 +0,0 @@ -- Proof General can now display Coq-generated diffs between proof steps - in color. (`#10019 <https://github.com/coq/coq/pull/10019>`_ and (in Proof General) - `#421 <https://github.com/ProofGeneral/PG/pull/421>`_, by Jim Fehrle). diff --git a/doc/common/styles/html/coqremote/cover.html b/doc/common/styles/html/coqremote/cover.html index 5d151381ff..b7c83bd2f9 100644 --- a/doc/common/styles/html/coqremote/cover.html +++ b/doc/common/styles/html/coqremote/cover.html @@ -52,7 +52,7 @@ <h2 style="text-align:center; font-size: 150%">The Coq Development Team</h2> <br /><br /><br /> -<p style="text-indent:0pt">Copyright © INRIA 1999-2017</p> +<p style="text-indent:0pt">Copyright © 1999-2019, Inria, CNRS and contributors</p> <p style="text-indent:0pt">This material may be distributed only subject to the terms and conditions set forth in the Open Publication License, v1.0 or later (the latest version is presently available at <a href="http://www.opencontent.org/openpub">http://www.opencontent.org/openpub</a>). Options A and B are not elected.</p> diff --git a/doc/common/styles/html/simple/cover.html b/doc/common/styles/html/simple/cover.html index 6053131045..28ce2eb087 100644 --- a/doc/common/styles/html/simple/cover.html +++ b/doc/common/styles/html/simple/cover.html @@ -30,7 +30,7 @@ <br /><br /><br /> -<p style="text-indent:0pt">Copyright © INRIA 1999-2017</p> +<p style="text-indent:0pt">Copyright © 1999-2019, Inria, CNRS and contributors</p> <p style="text-indent: 0pt">This material may be distributed only subject to the terms and conditions set forth in the Open Publication License, v1.0 or later (the latest version is presently available at <a href="http://www.opencontent.org/openpub">http://www.opencontent.org/openpub</a>). Options A and B are not elected.</p> diff --git a/doc/common/title.tex b/doc/common/title.tex index 76e50f65d2..2a104a87e6 100644 --- a/doc/common/title.tex +++ b/doc/common/title.tex @@ -43,9 +43,7 @@ $\pi r^2$ Project (formerly LogiCal, then TypiCal) V\coqversion, \today \par\vspace{20pt} %END LATEX -\copyright INRIA 1999-2004 ({\Coq} versions 7.x) - -\copyright INRIA 2004-2017 ({\Coq} versions 8.x) +\copyright 1999-2019, Inria, CNRS and contributors #3 \end{flushleft} diff --git a/doc/plugin_tutorial/tuto1/src/simple_declare.ml b/doc/plugin_tutorial/tuto1/src/simple_declare.ml index eb8161c2bb..9dd4700db5 100644 --- a/doc/plugin_tutorial/tuto1/src/simple_declare.ml +++ b/doc/plugin_tutorial/tuto1/src/simple_declare.ml @@ -1,14 +1,12 @@ -let edeclare ?hook ident (_, poly, _ as k) ~opaque sigma udecl body tyopt imps = +let edeclare ?hook ~name ~poly ~scope ~kind ~opaque sigma udecl body tyopt imps = let sigma, ce = DeclareDef.prepare_definition ~allow_evars:false ~opaque ~poly sigma udecl ~types:tyopt ~body in let uctx = Evd.evar_universe_context sigma in let ubinders = Evd.universe_binders sigma in let hook_data = Option.map (fun hook -> hook, uctx, []) hook in - DeclareDef.declare_definition ident k ce ubinders imps ?hook_data + DeclareDef.declare_definition ~name ~scope ~kind ubinders ce imps ?hook_data -let declare_definition ~poly ident sigma body = - let k = Decl_kinds.(Global ImportDefaultBehavior, poly, Definition) in +let declare_definition ~poly name sigma body = let udecl = UState.default_univ_decl in - edeclare ident k ~opaque:false sigma udecl body None [] - -(* But this definition cannot be undone by Reset ident *) + edeclare ~name ~poly ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) + ~kind:Decls.Definition ~opaque:false sigma udecl body None [] diff --git a/doc/plugin_tutorial/tuto1/src/simple_print.ml b/doc/plugin_tutorial/tuto1/src/simple_print.ml index 48b5f2214c..ba989b1bac 100644 --- a/doc/plugin_tutorial/tuto1/src/simple_print.ml +++ b/doc/plugin_tutorial/tuto1/src/simple_print.ml @@ -12,6 +12,6 @@ let simple_body_access gref = | Globnames.ConstRef cst -> let cb = Environ.lookup_constant cst (Global.env()) in match Global.body_of_constant_body Library.indirect_accessor cb with - | Some(e, _) -> EConstr.of_constr e + | Some(e, _, _) -> EConstr.of_constr e | None -> failwith "This term has no value" diff --git a/doc/plugin_tutorial/tuto2/_CoqProject b/doc/plugin_tutorial/tuto2/_CoqProject index cf9cb5cc26..0d7a644271 100644 --- a/doc/plugin_tutorial/tuto2/_CoqProject +++ b/doc/plugin_tutorial/tuto2/_CoqProject @@ -1,6 +1,15 @@ --R theories/ Tuto +-R theories Tuto2 -I src -theories/Test.v -src/demo.mlg -src/demo_plugin.mlpack +theories/Loader.v +theories/Demo.v +theories/Count.v + +src/custom.ml +src/custom.mli +src/counter.ml +src/counter.mli +src/persistent_counter.ml +src/persistent_counter.mli +src/g_tuto2.mlg +src/tuto2_plugin.mlpack diff --git a/doc/plugin_tutorial/tuto2/src/counter.ml b/doc/plugin_tutorial/tuto2/src/counter.ml new file mode 100644 index 0000000000..8721090d42 --- /dev/null +++ b/doc/plugin_tutorial/tuto2/src/counter.ml @@ -0,0 +1,22 @@ +(* + * This file defines our counter, which we use in the Count command. + *) + +(* + * Our counter is simply a reference called "counter" to an integer. + * + * Summary.ref behaves like ref, but also registers a summary to Coq. + *) +let counter = Summary.ref ~name:"counter" 0 + +(* + * We can increment our counter: + *) +let increment () = + counter := succ !counter + +(* + * We can also read the value of our counter: + *) +let value () = + !counter diff --git a/doc/plugin_tutorial/tuto2/src/counter.mli b/doc/plugin_tutorial/tuto2/src/counter.mli new file mode 100644 index 0000000000..984bc1d2cc --- /dev/null +++ b/doc/plugin_tutorial/tuto2/src/counter.mli @@ -0,0 +1,13 @@ +(* + * This file defines our counter, which we use in the Count command. + *) + +(* + * Increment the counter + *) +val increment : unit -> unit + +(* + * Determine the value of the counter + *) +val value : unit -> int diff --git a/doc/plugin_tutorial/tuto2/src/custom.ml b/doc/plugin_tutorial/tuto2/src/custom.ml new file mode 100644 index 0000000000..648786d3bd --- /dev/null +++ b/doc/plugin_tutorial/tuto2/src/custom.ml @@ -0,0 +1,5 @@ +(* + * This file defines a custom type for the PassCustom command. + *) + +type custom_type = Foo | Bar diff --git a/doc/plugin_tutorial/tuto2/src/custom.mli b/doc/plugin_tutorial/tuto2/src/custom.mli new file mode 100644 index 0000000000..648786d3bd --- /dev/null +++ b/doc/plugin_tutorial/tuto2/src/custom.mli @@ -0,0 +1,5 @@ +(* + * This file defines a custom type for the PassCustom command. + *) + +type custom_type = Foo | Bar diff --git a/doc/plugin_tutorial/tuto2/src/demo.mlg b/doc/plugin_tutorial/tuto2/src/demo.mlg deleted file mode 100644 index 966c05acdc..0000000000 --- a/doc/plugin_tutorial/tuto2/src/demo.mlg +++ /dev/null @@ -1,375 +0,0 @@ -(* -------------------------------------------------------------------------- *) -(* *) -(* Initial ritual dance *) -(* *) -(* -------------------------------------------------------------------------- *) - -DECLARE PLUGIN "demo_plugin" - -(* - Use this macro before any of the other OCaml macros. - - Each plugin has a unique name. - We have decided to name this plugin as "demo_plugin". - That means that: - - (1) If we want to load this particular plugin to Coq toplevel, - we must use the following command. - - Declare ML Module "demo_plugin". - - (2) The above command will succeed only if there is "demo_plugin.cmxs" - in some of the directories that Coq is supposed to look - (i.e. the ones we specified via "-I ..." command line options). - - (3) The file "demo_plugin.mlpack" lists the OCaml modules to be linked in - "demo_plugin.cmxs". - - (4) The file "demo_plugin.mlpack" as well as all .ml, .mli and .mlg files - are listed in the "_CoqProject" file. -*) - -(* -------------------------------------------------------------------------- *) -(* *) -(* How to define a new Vernacular command? *) -(* *) -(* -------------------------------------------------------------------------- *) - -VERNAC COMMAND EXTEND Cmd1 CLASSIFIED AS QUERY -| [ "Cmd1" ] -> { () } -END - -(* - These: - - VERNAC COMMAND EXTEND - - and - - END - - mark the beginning and the end of the definition of a new Vernacular command. - - Cmd1 is a unique identifier (which must start with an upper-case letter) - associated with the new Vernacular command we are defining. - - CLASSIFIED AS QUERY tells Coq that the new Vernacular command: - - changes neither the global environment - - nor does it modify the plugin's state. - - If the new command could: - - change the global environment - - or modify a plugin's state - then one would have to use CLASSIFIED AS SIDEFF instead. - - This: - - [ "Cmd1" ] -> { () } - - defines: - - the parsing rule - - the interpretation rule - - The parsing rule and the interpretation rule are separated by -> token. - - The parsing rule, in this case, is: - - [ "Cmd1" ] - - By convention, all vernacular command start with an upper-case letter. - - The [ and ] characters mark the beginning and the end of the parsing rule. - The parsing rule itself says that the syntax of the newly defined command - is composed from a single terminal Cmd1. - - The interpretation rule, in this case, is: - - { () } - - Similarly to the case of the parsing rule, - { and } characters mark the beginning and the end of the interpretation rule. - In this case, the following Ocaml expression: - - () - - defines the effect of the Vernacular command we have just defined. - That is, it behaves is no-op. -*) - -(* -------------------------------------------------------------------------- *) -(* *) -(* How to define a new Vernacular command with some terminal parameters? *) -(* *) -(* -------------------------------------------------------------------------- *) - -VERNAC COMMAND EXTEND Cmd2 CLASSIFIED AS QUERY -| [ "Cmd2" "With" "Some" "Terminal" "Parameters" ] -> { () } -END - -(* - As shown above, the Vernacular command can be composed from - any number of terminals. - - By convention, each of these terminals starts with an upper-case letter. -*) - -(* -------------------------------------------------------------------------- *) -(* *) -(* How to define a new Vernacular command with some non-terminal parameter? *) -(* *) -(* -------------------------------------------------------------------------- *) - -{ - -open Stdarg - -} - -VERNAC COMMAND EXTEND Cmd3 CLASSIFIED AS QUERY -| [ "Cmd3" int(i) ] -> { () } -END - -(* - This: - - open Stdarg - - is needed as some identifiers in the Ocaml code generated by the - - VERNAC COMMAND EXTEND ... END - - macros are not fully qualified. - - This: - - int(i) - - means that the new command is expected to be followed by an integer. - The integer is bound in the parsing rule to variable i. - This variable i then can be used in the interpretation rule. - - To see value of which Ocaml types can be bound this way, - look at the wit_* function declared in interp/stdarg.mli - (in the Coq's codebase). - - If we drop the wit_ prefix, we will get the token - that we can use in the parsing rule. - That is, since there exists wit_int, we know that - we can write: - - int(i) - - By looking at the signature of the wit_int function: - - val wit_int : int uniform_genarg_type - - we also know that variable i will have the type int. - - The types of wit_* functions are either: - - 'c uniform_genarg_type - - or - - ('a,'b,'c) genarg_type - - In both cases, the bound variable will have type 'c. -*) - -(* -------------------------------------------------------------------------- *) -(* *) -(* How to define a new Vernacular command with variable number of arguments? *) -(* *) -(* -------------------------------------------------------------------------- *) - -VERNAC COMMAND EXTEND Cmd4 CLASSIFIED AS QUERY -| [ "Cmd4" int_list(l) ] -> { () } -END - -(* - This: - - int_list(l) - - means that the new Vernacular command is expected to be followed - by a (whitespace separated) list of integers. - This list of integers is bound to the indicated l. - - In this case, as well as in the cases we point out below, instead of int - in int_list we could use any other supported type, e.g. ident, bool, ... - - To see which other Ocaml type constructors (in addition to list) - are supported, have a look at the parse_user_entry function defined - in grammar/q_util.mlp file. - - E.g.: - - ne_int_list(x) would represent a non-empty list of integers, - - int_list(x) would represent a list of integers, - - int_opt(x) would represent a value of type int option, - - ··· -*) - -(* -------------------------------------------------------------------------- *) -(* *) -(* How to define a new Vernacular command that takes values of a custom type? *) -(* *) -(* -------------------------------------------------------------------------- *) - -{ - -open Ltac_plugin - -} - -(* - If we want to avoid a compilation failure - - "no implementation available for Tacenv" - - then we have to open the Ltac_plugin module. -*) - -(* - Pp module must be opened because some of the macros that are part of the API - do not expand to fully qualified names. -*) - -{ - -type type_5 = Foo_5 | Bar_5 - -} - -(* - We define a type of values that we want to pass to our Vernacular command. -*) - -(* - By default, we are able to define new Vernacular commands that can take - parameters of some of the supported types. Which types are supported, - that was discussed earlier. - - If we want to be able to define Vernacular command that takes parameters - of a type that is not supported by default, we must use the following macro: -*) - -{ - -open Pp - -} - -VERNAC ARGUMENT EXTEND custom5 -| [ "Foo_5" ] -> { Foo_5 } -| [ "Bar_5" ] -> { Bar_5 } -END - -(* - where: - - custom5 - - indicates that, from now on, in our parsing rules we can write: - - custom5(some_variable) - - in those places where we expect user to provide an input - that can be parsed by the parsing rules above - (and interpreted by the interpretations rules above). -*) - -(* Here: *) - -VERNAC COMMAND EXTEND Cmd5 CLASSIFIED AS QUERY -| [ "Cmd5" custom5(x) ] -> { () } -END - -(* - we define a new Vernacular command whose parameters, provided by the user, - can be mapped to values of type_5. -*) - -(* -------------------------------------------------------------------------- *) -(* *) -(* How to give a feedback to the user? *) -(* *) -(* -------------------------------------------------------------------------- *) - -VERNAC COMMAND EXTEND Cmd6 CLASSIFIED AS QUERY -| [ "Cmd6" ] -> { Feedback.msg_notice (Pp.str "Everything is awesome!") } -END - -(* - The following functions: - - - Feedback.msg_info : Pp.t -> unit - - Feedback.msg_notice : Pp.t -> unit - - Feedback.msg_warning : Pp.t -> unit - - Feedback.msg_error : Pp.t -> unit - - Feedback.msg_debug : Pp.t -> unit - - enable us to give user a textual feedback. - - Pp module enable us to represent and construct pretty-printing instructions. - The concepts defined and the services provided by the Pp module are in - various respects related to the concepts and services provided - by the Format module that is part of the Ocaml standard library. -*) - -(* -------------------------------------------------------------------------- *) -(* *) -(* How to implement a Vernacular command with (undoable) side-effects? *) -(* *) -(* -------------------------------------------------------------------------- *) - -{ - -open Summary.Local - -} - -(* - By opening Summary.Local module we shadow the original functions - that we traditionally use for implementing stateful behavior. - - ref - ! - := - - are now shadowed by their counterparts in Summary.Local. *) - -{ - -let counter = ref ~name:"counter" 0 - -} - -VERNAC COMMAND EXTEND Cmd7 CLASSIFIED AS SIDEFF -| [ "Cmd7" ] -> { counter := succ !counter; - Feedback.msg_notice (Pp.str "counter = " ++ Pp.str (string_of_int (!counter))) } -END - -TACTIC EXTEND tactic1 -| [ "tactic1" ] -> { Proofview.tclUNIT () } -END - -(* ---- *) - -{ - -type custom = Foo_2 | Bar_2 - -let pr_custom _ _ _ = function - | Foo_2 -> Pp.str "Foo_2" - | Bar_2 -> Pp.str "Bar_2" - -} - -ARGUMENT EXTEND custom2 PRINTED BY { pr_custom } -| [ "Foo_2" ] -> { Foo_2 } -| [ "Bar_2" ] -> { Bar_2 } -END - -TACTIC EXTEND tactic2 -| [ "tactic2" custom2(x) ] -> { Proofview.tclUNIT () } -END diff --git a/doc/plugin_tutorial/tuto2/src/demo_plugin.mlpack b/doc/plugin_tutorial/tuto2/src/demo_plugin.mlpack deleted file mode 100644 index 4f0b8480b5..0000000000 --- a/doc/plugin_tutorial/tuto2/src/demo_plugin.mlpack +++ /dev/null @@ -1 +0,0 @@ -Demo diff --git a/doc/plugin_tutorial/tuto2/src/dune b/doc/plugin_tutorial/tuto2/src/dune index f2bc405455..68ddd13947 100644 --- a/doc/plugin_tutorial/tuto2/src/dune +++ b/doc/plugin_tutorial/tuto2/src/dune @@ -4,6 +4,6 @@ (libraries coq.plugins.ltac)) (rule - (targets demo.ml) - (deps (:pp-file demo.mlg) ) + (targets g_tuto2.ml) + (deps (:pp-file g_tuto2.mlg) ) (action (run coqpp %{pp-file}))) diff --git a/doc/plugin_tutorial/tuto2/src/g_tuto2.mlg b/doc/plugin_tutorial/tuto2/src/g_tuto2.mlg new file mode 100644 index 0000000000..a3ce60d432 --- /dev/null +++ b/doc/plugin_tutorial/tuto2/src/g_tuto2.mlg @@ -0,0 +1,618 @@ +(* -------------------------------------------------------------------------- *) +(* *) +(* Initial ritual dance *) +(* *) +(* -------------------------------------------------------------------------- *) + +DECLARE PLUGIN "tuto2_plugin" + +(* + Use this macro before any of the other OCaml macros. + + Each plugin has a unique name. + We have decided to name this plugin as "tuto2_plugin". + That means that: + + (1) We write the following command in a file called Loader.v: + + Declare ML Module "tuto2_plugin". + + to load this command into the Coq top-level. + + (2) Users can then load our plugin in other Coq files by writing: + + From Tuto2 Require Import Loader. + + where Loader is the name of the file that declares "tuto2_plugin", + and where Tuto2 is the name passed to the -R argument in our _CoqProject. + + (3) The above commands will succeed only if there is "tuto2_plugin.cmxs" + in some of the directories where Coq is supposed to look + (i.e. the ones we specified via "-I ..." command line options in + _CoqProject). As long as this is listed in our _CoqProject, the + Makefile takes care of placing it in the right directory. + + (4) The file "tuto2_plugin.mlpack" lists the OCaml modules to be linked in + "tuto2_plugin.cmxs". + + (5) The file "tuto2_plugin.mlpack" as well as all .ml, .mli and .mlg files + are listed in the "_CoqProject" file. + *) + +(* -------------------------------------------------------------------------- *) +(* *) +(* Importing OCaml dependencies *) +(* *) +(* -------------------------------------------------------------------------- *) + +(* + * This .mlg file is parsed into a .ml file. You can put OCaml in this file + * inside of curly braces. It's best practice to use this only to import + * other modules, and include most of your functionality in those modules. + * + * Here we list all of the dependencies that these commands have, and explain + * why. We also refer to the first command that uses them, where further + * explanation can be found in context. + *) +{ + (*** Dependencies from Coq ***) + + (* + * This lets us take non-terminal arguments to a command (for example, + * the PassInt command that takes an integer argument needs this + * this dependency). + * + * First used by: PassInt + *) + open Stdarg + + (* + * This is Coq's pretty-printing module. Here, we need it to use some + * useful syntax for pretty-printing. + * + * First use by: Count + *) + open Pp +} + +(* -------------------------------------------------------------------------- *) +(* *) +(* How to define a new Vernacular command? *) +(* *) +(* -------------------------------------------------------------------------- *) + +(* + This command does nothing: +*) +VERNAC COMMAND EXTEND NoOp CLASSIFIED AS QUERY +| [ "Nothing" ] -> { () } +END + +(* + --- Defining a Command --- + + These: + + VERNAC COMMAND EXTEND + + and + + END + + mark the beginning and the end of the definition of a new Vernacular command. + + --- Assigning a Command a Unique Identifier --- + + NoOp is a unique identifier (which must start with an upper-case letter) + associated with the new Vernacular command we are defining. It is good + to make this identifier descriptive. + + --- Classifying a Command --- + + CLASSIFIED AS QUERY tells Coq that the new Vernacular command neither: + - changes the global environment, nor + - modifies the plugin's state. + + If the new command could: + - change the global environment + - or modify a plugin's state + then one would have to use CLASSIFIED AS SIDEFF instead. + + --- Defining Parsing and Interpretation Rules --- + + This: + + [ "Nothing" ] -> { () } + + defines: + - the parsing rule (left) + - the interpretation rule (right) + + The parsing rule and the interpretation rule are separated by -> token. + + The parsing rule, in this case, is: + + [ "Nothing" ] + + By convention, all vernacular command start with an upper-case letter. + + The '[' and ']' characters mark the beginning and the end of the parsing + rule, respectively. The parsing rule itself says that the syntax of the + newly defined command is composed from a single terminal Nothing. + + The interpretation rule, in this case, is: + + { () } + + Similarly to the case of the parsing rule, the + '{' and '}' characters mark the beginning and the end of the interpretation + rule. In this case, the following Ocaml expression: + + () + + defines the effect of the Vernacular command we have just defined. + That is, it behaves is no-op. + + --- Calling a Command --- + + In Demo.v, we call this command by writing: + + Nothing. + + since our parsing rule is "Nothing". This does nothing, since our + interpretation rule is (). +*) + +(* -------------------------------------------------------------------------- *) +(* *) +(* How to define a new Vernacular command with some terminal parameters? *) +(* *) +(* -------------------------------------------------------------------------- *) + +(* + This command takes some terminal parameters and does nothing. +*) +VERNAC COMMAND EXTEND NoOpTerminal CLASSIFIED AS QUERY +| [ "Command" "With" "Some" "Terminal" "Parameters" ] -> { () } +END + +(* + --- Defining a Command with Terminal Parameters --- + + As shown above, the Vernacular command can be composed from + any number of terminals. + + By convention, each of these terminals starts with an upper-case letter. + + --- Calling a Command with Terminal Parameters --- + + In Demo.v, we call this command by writing: + + Command With Some Terminal Parameters. + + to match our parsing rule. As expected, this does nothing. + + --- Recognizing Syntax Errors --- + + Note that if we were to omit any of these terminals, for example by writing: + + Command. + + it would fail to parse (as expected), showing this error to the user: + + Syntax error: illegal begin of vernac. +*) + +(* -------------------------------------------------------------------------- *) +(* *) +(* How to define a new Vernacular command with some non-terminal parameter? *) +(* *) +(* -------------------------------------------------------------------------- *) + +(* + This command takes an integer argument and does nothing. +*) +VERNAC COMMAND EXTEND PassInt CLASSIFIED AS QUERY +| [ "Pass" int(i) ] -> { () } +END + +(* + --- Dependencies --- + + Since this command takes a non-terminal argument, it is the first + to depend on Stdarg (opened at the top of this file). + + --- Defining a Command with Non-Terminal Arguments --- + + This: + + int(i) + + means that the new command is expected to be followed by an integer. + The integer is bound in the parsing rule to variable i. + This variable i then can be used in the interpretation rule. + + To see value of which Ocaml types can be bound this way, + look at the wit_* function declared in interp/stdarg.mli + (in the Coq's codebase). There are more examples in tuto1. + + If we drop the wit_ prefix, we will get the token + that we can use in the parsing rule. + That is, since there exists wit_int, we know that + we can write: + + int(i) + + By looking at the signature of the wit_int function: + + val wit_int : int uniform_genarg_type + + we also know that variable i will have the type int. + + --- Recognizing Build Errors --- + + The mapping from int(i) to wit_int is automatic. + This is why, if we forget to open Stdarg, we will get this error: + + Unbound value wit_int + + when we try to build our plugin. It is good to recognize this error, + since this is a common mistake in plugin development, and understand + that the fix is to open the file (Stdarg) where wit_int is defined. + + --- Calling a Command with Terminal Arguments --- + + We call this command in Demo.v by writing: + + Pass 42. + + We could just as well pass any other integer. As expected, this command + does nothing. + + --- Recognizing Syntax Errors --- + + As in our previous command, if we were to omit the arguments to the command, + for example by writing: + + Pass. + + it would fail to parse (as expected), showing this error to the user: + + Syntax error: [prim:integer] expected after 'Pass' (in [vernac:command]). + + The same thing would happen if we passed the wrong argument type: + + Pass True. + + If we pass too many arguments: + + Pass 15 20. + + we will get a different syntax error: + + Syntax error: '.' expected after [vernac:command] (in [vernac_aux]). + + It is good to recognize these errors, since doing so can help you + catch mistakes you make defining your parser rules during plugin + development. +*) + +(* -------------------------------------------------------------------------- *) +(* *) +(* How to define a new Vernacular command with variable number of arguments? *) +(* *) +(* -------------------------------------------------------------------------- *) + +(* + This command takes a list of integers and does nothing: +*) +VERNAC COMMAND EXTEND AcceptIntList CLASSIFIED AS QUERY +| [ "Accept" int_list(l) ] -> { () } +END + +(* + --- Dependencies --- + + Much like PassInt, this command depends on Stdarg. + + --- Defining a Command that Takes a Variable Number of Arguments --- + + This: + + int_list(l) + + means that the new Vernacular command is expected to be followed + by a (whitespace separated) list of integers. + This list of integers is bound to the indicated l. + + In this case, as well as in the cases we point out below, instead of int + in int_list we could use any other supported type, e.g. ident, bool, ... + + --- Other Ways to Take a Variable Number of Arguments --- + + To see which other Ocaml type constructors (in addition to list) + are supported, have a look at the parse_user_entry function defined + in the coqpp/coqpp_parse.mly file. + + E.g.: + - ne_int_list(x) would represent a non-empty list of integers, + - int_list(x) would represent a list of integers, + - int_opt(x) would represent a value of type int option, + - ··· + + Much like with int_list, we could use any other supported type here. + There are some more examples of this in tuto1. + + --- Calling a Command with a Variable Number of Arguments --- + + We call this command in Demo.v by writing: + + Accept 100 200 300 400. + + As expected, this does nothing. + + Since our parser rule uses int_list, the arguments to Accept can be a + list of integers of any length. For example, we can pass the empty list: + + Accept. + + or just one argument: + + Accept 2. + + and so on. +*) + +(* -------------------------------------------------------------------------- *) +(* *) +(* How to define a new Vernacular command that takes values of a custom type? *) +(* *) +(* -------------------------------------------------------------------------- *) + +(* + --- Defining Custom Types --- + + Vernacular commands can take custom types in addition to the built-in + ones. The first step to taking these custom types as arguments is + to define them. + + + We define a type of values that we want to pass to our Vernacular command + in custom.ml/custom.mli. The type is very simple: + + type custom_type : Foo | Bar. + + --- Using our New Module --- + + Now that we have a new OCaml module Custom, in order to use it, we must + do the following: + + 1. Add src/custom.ml and src/custom.mli to our _CoqProject + 2. Add Custom to our tuto2_plugin.mlpack + + This workflow will become very familiar to you when you add new modules + to your plugins, so it is worth getting used to. + + --- Depending on our New Module --- + + Now that our new module is listed in both _CoqProject and tuto2_plugin.mlpack, + we can use fully qualified names Custom.Foo and Custom.Bar. + + Alternatively, we could add the dependency on our module: + + open Custom. + + to the top of the file, and then refer to Foo and Bar directly. + + --- Telling Coq About our New Argument Type --- + + By default, we are able to define new Vernacular commands that can take + parameters of some of the supported types. Which types are supported, + that was discussed earlier. + + If we want to be able to define Vernacular command that takes parameters + of a type that is not supported by default, we must use the following macro: +*) +VERNAC ARGUMENT EXTEND custom +| [ "Foo" ] -> { Custom.Foo } +| [ "Bar" ] -> { Custom.Bar } +END + +(* + where: + + custom + + indicates that, from now on, in our parsing rules we can write: + + custom(some_variable) + + in those places where we expect user to provide an input + that can be parsed by the parsing rules above + (and interpreted by the interpretations rules above). +*) + +(* + --- Defining a Command that Takes an Argument of a Custom Type --- + + Now that Coq is aware of our new argument type, we can define a command + that uses it. This command takes an argument Foo or Bar and does nothing: +*) +VERNAC COMMAND EXTEND PassCustom CLASSIFIED AS QUERY +| [ "Foobar" custom(x) ] -> { () } +END + +(* + --- Calling a Command that Takes an Argument of a Custom Type --- + + We call this command in Demo.v by writing: + + Foobar Foo. + Foobar Bar. + + As expected, both of these do nothing. In the first case, x gets + the value Custom.Foo : Custom.custom_type, since our custom parsing + and interpretation rules (VERNAC ARGUMENT EXTEND custom ...) map + the input Foo to Custom.Foo. Similarly, in the second case, x gets + the value Custom.Bar : Custom.custom_type. +*) + +(* -------------------------------------------------------------------------- *) +(* *) +(* How to give a feedback to the user? *) +(* *) +(* -------------------------------------------------------------------------- *) + +(* + So far we have defined commands that do nothing. + We can also signal feedback to the user. + + This command tells the user that everything is awesome: +*) +VERNAC COMMAND EXTEND Awesome CLASSIFIED AS QUERY +| [ "Is" "Everything" "Awesome" ] -> + { + Feedback.msg_notice (Pp.str "Everything is awesome!") + } +END + +(* + --- Pretty Printing --- + + User feedback functions like Feedback.msg_notice take a Pp.t as an argument. + Check the Pp module to see which functions are available to construct + a Pp.t. + + The Pp module enable us to represent and construct pretty-printing + instructions. The concepts defined and the services provided by the + Pp module are in various respects related to the concepts and services + provided by the Format module that is part of the Ocaml standard library. + + --- Giving Feedback --- + + Once we have a Pp.t, we can use the following functions: + + - Feedback.msg_info : Pp.t -> unit + - Feedback.msg_notice : Pp.t -> unit + - Feedback.msg_warning : Pp.t -> unit + - Feedback.msg_debug : Pp.t -> unit + + to give user a textual feedback. Examples of some of these can be + found in tuto0. + + --- Signaling Errors --- + + While there is a Feedback.msg_error, when signaling an error, + it is currently better practice to use user_err. There is an example of + this in tuto0. +*) + +(* -------------------------------------------------------------------------- *) +(* *) +(* How to implement a Vernacular command with (undoable) side-effects? *) +(* *) +(* -------------------------------------------------------------------------- *) + +(* + This command counts how many times it has been called since importing + our plugin, and signals that information to the user: + *) +VERNAC COMMAND EXTEND Count CLASSIFIED AS SIDEFF +| [ "Count" ] -> + { + Counter.increment (); + let v = Counter.value () in + Feedback.msg_notice (Pp.str "Times Count has been called: " ++ Pp.int v) + } +END + +(* + --- Dependencies --- + + If we want to use the ++ syntax, then we need to depend on Pp explicitly. + This is why, at the top, we write: + + open Pp. + + --- Defining the Counter --- + + We define our counter in the Counter module. Please see counter.ml and + counter.mli for details. + + As with Custom, we must modify our _CoqProject and tuto2_plugin.mlpack + so that we can use Counter in our code. + + --- Classifying the Command --- + + This command has undoable side-effects: When the plugin is first loaded, + the counter is instantiated to 0. After each time we call Count, the value of + the counter increases by 1. + + Thus, we must write CLASSIFIED AS SIDEEFF for this command, rather than + CLASSIFIED AS QUERY. See the explanation from the NoOp command earlier if + you do not remember the distinction. + + --- Calling the Command --- + + We call our command three times in Demo.v by writing: + + Count. + Count. + Count. + + This gives us the following output: + + Times Count has been called: 1 + Times Count has been called: 2 + Times Count has been called: 3 + + Note that when the plugin is first loaded, the counter is 0. It increases + each time Count is called. + + --- Behavior with Imports --- + + Count.v shows the behavior with imports. Note that if we import Demo.v, + the counter is set to 0 from the beginning, even though Demo.v calls + Count three times. + + In other words, this is not persistent! +*) + +(* -------------------------------------------------------------------------- *) +(* *) +(* How to implement a Vernacular command that uses persistent storage? *) +(* *) +(* -------------------------------------------------------------------------- *) + +(* + * This command is like Count, but it is persistent across modules: + *) +VERNAC COMMAND EXTEND CountPersistent CLASSIFIED AS SIDEFF +| [ "Count" "Persistent" ] -> + { + Persistent_counter.increment (); + let v = Persistent_counter.value () in + Feedback.msg_notice (Pp.str "Times Count Persistent has been called: " ++ Pp.int v) + } +END + +(* + --- Persistent Storage --- + + Everything is similar to the Count command, except that we use a counter + that is persistent. See persistent_counter.ml for details. + + The key trick is that we must create a persistent object for our counter + to persist across modules. Coq has some useful APIs for this in Libobject. + We demonstrate these in persistent_counter.ml. + + This is really, really useful if you want, for example, to cache some + results that your plugin computes across modules. A persistent object + can be a hashtable, for example, that maps inputs to outputs your command + has already computed, if you know the result will not change. + + --- Calling the Command --- + + We call the command in Demo.v and in Count.v, just like we did with Count. + Note that this time, the value of the counter from Demo.v persists in Count.v. +*) diff --git a/doc/plugin_tutorial/tuto2/src/persistent_counter.ml b/doc/plugin_tutorial/tuto2/src/persistent_counter.ml new file mode 100644 index 0000000000..868f6ab99b --- /dev/null +++ b/doc/plugin_tutorial/tuto2/src/persistent_counter.ml @@ -0,0 +1,56 @@ +(* + * This file defines our persistent counter, which we use in the + * CountPersistent command. + *) + +(* + * At its core, our persistent counter looks exactly the same as + * our non-persistent counter (with a different name to prevent collisions): + *) +let counter = Summary.ref ~name:"persistent_counter" 0 + +(* + * The difference is that we need to declare it as a persistent object + * using Libobject.declare_object. To do that, we define a function that + * saves the value that is passed to it into the reference we have just defined: + *) +let cache_count (_, v) = + counter := v + +(* + * We then use declare_object to create a function that takes an integer value + * (the type our counter refers to) and creates a persistent object from that + * value: + *) +let declare_counter : int -> Libobject.obj = + let open Libobject in + declare_object + { + (default_object "COUNTER") with + cache_function = cache_count; + load_function = (fun _ -> cache_count); + } +(* + * See Libobject for more information on what other information you + * can pass here, and what all of these functions mean. + * + * For example, if we passed the same thing that we pass to load_function + * to open_function, then our last call to Count Persistent in Count.v + * would return 4 and not 6. + *) + +(* + * Incrementing our counter looks almost identical: + *) +let increment () = + Lib.add_anonymous_leaf (declare_counter (succ !counter)) +(* + * except that we must call our declare_counter function to get a persistent + * object. We then pass this object to Lib.add_anonymous_leaf. + *) + +(* + * Reading a value does not change at all: + *) +let value () = + !counter diff --git a/doc/plugin_tutorial/tuto2/src/persistent_counter.mli b/doc/plugin_tutorial/tuto2/src/persistent_counter.mli new file mode 100644 index 0000000000..d3c88e19a6 --- /dev/null +++ b/doc/plugin_tutorial/tuto2/src/persistent_counter.mli @@ -0,0 +1,14 @@ +(* + * This file defines our persistent counter, which we use in the + * CountPersistent command. + *) + +(* + * Increment the persistent counter + *) +val increment : unit -> unit + +(* + * Determine the value of the persistent counter + *) +val value : unit -> int diff --git a/doc/plugin_tutorial/tuto2/src/tuto2_plugin.mlpack b/doc/plugin_tutorial/tuto2/src/tuto2_plugin.mlpack new file mode 100644 index 0000000000..0bc7402978 --- /dev/null +++ b/doc/plugin_tutorial/tuto2/src/tuto2_plugin.mlpack @@ -0,0 +1,4 @@ +Custom +Counter +Persistent_counter +G_tuto2 diff --git a/doc/plugin_tutorial/tuto2/theories/Count.v b/doc/plugin_tutorial/tuto2/theories/Count.v new file mode 100644 index 0000000000..3287342b75 --- /dev/null +++ b/doc/plugin_tutorial/tuto2/theories/Count.v @@ -0,0 +1,19 @@ +Require Import Demo. + +(*** Local ***) + +Count. +Count. + +Import Demo. + +Count. + +(*** Persistent ***) + +Count Persistent. +Count Persistent. + +Import Demo. + +Count Persistent. diff --git a/doc/plugin_tutorial/tuto2/theories/Demo.v b/doc/plugin_tutorial/tuto2/theories/Demo.v new file mode 100644 index 0000000000..73b5fcca62 --- /dev/null +++ b/doc/plugin_tutorial/tuto2/theories/Demo.v @@ -0,0 +1,63 @@ +From Tuto2 Require Import Loader. + +(*** A no-op command ***) + +Nothing. + +(*** No-op commands with arguments ***) + +(* + * Terminal parameters: + *) +Command With Some Terminal Parameters. +(* Command. *) (* does not parse *) + +(* + * A single non-terminal argument: + *) +Pass 42. +(* Pass. *) (* does not parse *) +(* Pass True. *) (* does not parse *) +(* Pass 15 20. *) (* does not parse *) + +(* + * A list of non-terminal arguments: + *) +Accept 100 200 300 400. +Accept. +Accept 2. + +(* + * A custom argument: + *) +Foobar Foo. +Foobar Bar. + +(*** Commands that give feedback ***) + +(* + * Simple feedback: + *) +Is Everything Awesome. + +(*** Storage and side effects ***) + +(* + * Local side effects: + *) +Count. +Count. +Count. +(* + * See Count.v for behavior in modules that import this one. + *) + +(* + * Persistent side effects: + *) +Count Persistent. +Count Persistent. +Count Persistent. +(* + * See Count.v for behavior in modules that import this one. + *) diff --git a/doc/plugin_tutorial/tuto2/theories/Loader.v b/doc/plugin_tutorial/tuto2/theories/Loader.v new file mode 100644 index 0000000000..9ce9991c86 --- /dev/null +++ b/doc/plugin_tutorial/tuto2/theories/Loader.v @@ -0,0 +1 @@ +Declare ML Module "tuto2_plugin". diff --git a/doc/plugin_tutorial/tuto2/theories/Test.v b/doc/plugin_tutorial/tuto2/theories/Test.v deleted file mode 100644 index 38e83bfff1..0000000000 --- a/doc/plugin_tutorial/tuto2/theories/Test.v +++ /dev/null @@ -1,19 +0,0 @@ -Declare ML Module "demo_plugin". - -Cmd1. -Cmd2 With Some Terminal Parameters. -Cmd3 42. -Cmd4 100 200 300 400. -Cmd5 Foo_5. -Cmd5 Bar_5. -Cmd6. -Cmd7. -Cmd7. -Cmd7. - -Goal True. -Proof. - tactic1. - tactic2 Foo_2. - tactic2 Bar_2. -Abort. diff --git a/doc/sphinx/_static/ansi-dark.css b/doc/sphinx/_static/ansi-dark.css index a564fd70bb..bbace7c553 100644 --- a/doc/sphinx/_static/ansi-dark.css +++ b/doc/sphinx/_static/ansi-dark.css @@ -1,6 +1,6 @@ /************************************************************************/ /* * The Coq Proof Assistant / The Coq Development Team */ -/* v * INRIA, CNRS and contributors - Copyright 1999-2018 */ +/* v * INRIA, CNRS and contributors - Copyright 1999-2019 */ /* <O___,, * (see CREDITS file for the list of authors) */ /* \VV/ **************************************************************/ /* // * This file is distributed under the terms of the */ diff --git a/doc/sphinx/_static/ansi.css b/doc/sphinx/_static/ansi.css index 26bd797709..b3b5341166 100644 --- a/doc/sphinx/_static/ansi.css +++ b/doc/sphinx/_static/ansi.css @@ -1,6 +1,6 @@ /************************************************************************/ /* * The Coq Proof Assistant / The Coq Development Team */ -/* v * INRIA, CNRS and contributors - Copyright 1999-2018 */ +/* v * INRIA, CNRS and contributors - Copyright 1999-2019 */ /* <O___,, * (see CREDITS file for the list of authors) */ /* \VV/ **************************************************************/ /* // * This file is distributed under the terms of the */ diff --git a/doc/sphinx/_static/coqdoc.css b/doc/sphinx/_static/coqdoc.css index bbcc044a20..7a3d59d4c0 100644 --- a/doc/sphinx/_static/coqdoc.css +++ b/doc/sphinx/_static/coqdoc.css @@ -1,6 +1,6 @@ /************************************************************************/ /* * The Coq Proof Assistant / The Coq Development Team */ -/* v * INRIA, CNRS and contributors - Copyright 1999-2018 */ +/* v * INRIA, CNRS and contributors - Copyright 1999-2019 */ /* <O___,, * (see CREDITS file for the list of authors) */ /* \VV/ **************************************************************/ /* // * This file is distributed under the terms of the */ diff --git a/doc/sphinx/_static/notations.css b/doc/sphinx/_static/notations.css index 8322ab0137..4a5fa0b328 100644 --- a/doc/sphinx/_static/notations.css +++ b/doc/sphinx/_static/notations.css @@ -1,6 +1,6 @@ /************************************************************************/ /* * The Coq Proof Assistant / The Coq Development Team */ -/* v * INRIA, CNRS and contributors - Copyright 1999-2018 */ +/* v * INRIA, CNRS and contributors - Copyright 1999-2019 */ /* <O___,, * (see CREDITS file for the list of authors) */ /* \VV/ **************************************************************/ /* // * This file is distributed under the terms of the */ diff --git a/doc/sphinx/_static/notations.js b/doc/sphinx/_static/notations.js index eb7f211e8b..63112312d0 100644 --- a/doc/sphinx/_static/notations.js +++ b/doc/sphinx/_static/notations.js @@ -1,6 +1,6 @@ /************************************************************************/ /* * The Coq Proof Assistant / The Coq Development Team */ -/* v * INRIA, CNRS and contributors - Copyright 1999-2018 */ +/* v * INRIA, CNRS and contributors - Copyright 1999-2019 */ /* <O___,, * (see CREDITS file for the list of authors) */ /* \VV/ **************************************************************/ /* // * This file is distributed under the terms of the */ diff --git a/doc/sphinx/_static/pre-text.css b/doc/sphinx/_static/pre-text.css index 38d81abefe..9d133fb1aa 100644 --- a/doc/sphinx/_static/pre-text.css +++ b/doc/sphinx/_static/pre-text.css @@ -1,6 +1,6 @@ /************************************************************************/ /* * The Coq Proof Assistant / The Coq Development Team */ -/* v * INRIA, CNRS and contributors - Copyright 1999-2018 */ +/* v * INRIA, CNRS and contributors - Copyright 1999-2019 */ /* <O___,, * (see CREDITS file for the list of authors) */ /* \VV/ **************************************************************/ /* // * This file is distributed under the terms of the */ diff --git a/doc/sphinx/addendum/implicit-coercions.rst b/doc/sphinx/addendum/implicit-coercions.rst index d5523e8561..7fee62179b 100644 --- a/doc/sphinx/addendum/implicit-coercions.rst +++ b/doc/sphinx/addendum/implicit-coercions.rst @@ -145,19 +145,25 @@ Declaring Coercions .. exn:: Cannot recognize @class as a source class of @qualid. :undocumented: - .. exn:: @qualid does not respect the uniform inheritance condition. + .. warn:: @qualid does not respect the uniform inheritance condition. :undocumented: .. exn:: Found target class ... instead of ... :undocumented: - .. warn:: Ambiguous path. + .. warn:: New coercion path ... is ambiguous with existing ... - When the coercion :token:`qualid` is added to the inheritance graph, - invalid coercion paths are ignored. The :cmd:`Coercion` command tries to check - that they are convertible with existing ones on the same classes. - The paths for which this check fails are displayed by a warning in the form - :g:`[f₁;..;fₙ] : C >-> D`. + When the coercion :token:`qualid` is added to the inheritance graph, new + coercion paths which have the same classes as existing ones are ignored. + The :cmd:`Coercion` command tries to check the convertibility of new ones and + existing ones. The paths for which this check fails are displayed by a warning + in the form :g:`[f₁;..;fₙ] : C >-> D`. + + The convertibility checking procedure for coercion paths is complete for + paths consisting of coercions satisfying the uniform inheritance condition, + but some coercion paths could be reported as ambiguous even if they are + convertible with existing ones when they have coercions that don't satisfy + the uniform inheritance condition. .. cmdv:: Local Coercion @qualid : @class >-> @class diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index db4ebd5e38..fd84868a1f 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -120,7 +120,9 @@ reference manual. Here are the most important user-visible changes: - CoqIDE: - - CoqIDE now depends on gtk+3 and lablgtk3 instead of gtk+2 and lablgtk2 + - CoqIDE now depends on gtk+3 and lablgtk3 instead of gtk+2 and lablgtk2. + The INSTALL file available in the Coq sources has been updated to list + the new dependencies (`#9279 <https://github.com/coq/coq/pull/9279>`_, by Hugo Herbelin, with help from Jacques Garrigue, Emilio Jesús Gallego Arias, Michael Sogetrop and Vincent Laporte). @@ -525,7 +527,13 @@ Other changes in 8.10+beta1 (`#9829 <https://github.com/coq/coq/pull/9829>`_, by Vincent Laporte). - :cmd:`Coercion` does not warn ambiguous paths which are obviously - convertible with existing ones + convertible with existing ones. The ambiguous paths messages have been + turned to warnings, thus now they could appear in the output of ``coqc``. + The convertibility checking procedure for coercion paths is complete for + paths consisting of coercions satisfying the uniform inheritance condition, + but some coercion paths could be reported as ambiguous even if they are + convertible with existing ones when they have coercions that don't satisfy + the uniform inheritance condition (`#9743 <https://github.com/coq/coq/pull/9743>`_, closes `#3219 <https://github.com/coq/coq/issues/3219>`_, by Kazuhiko Sakaguchi). @@ -596,6 +604,52 @@ Other changes in 8.10+beta1 with help and ideas from Emilio Jesús Gallego Arias, Gaëtan Gilbert, Clément Pit-Claudel, Matthieu Sozeau, and Enrico Tassi). +Changes in 8.10+beta2 +~~~~~~~~~~~~~~~~~~~~~ + +Many bug fixes and documentation improvements, in particular: + +**Tactics** + +- Make the :tacn:`discriminate` tactic work together with + :flag:`Universe Polymorphism` and equality in :g:`Type`. This, + in particular, makes :tacn:`discriminate` compatible with the HoTT + library https://github.com/HoTT/HoTT + (`#10205 <https://github.com/coq/coq/pull/10205>`_, + by Andreas Lynge, review by Pierre-Marie Pédrot and Matthieu Sozeau). + +**SSReflect** + +- Make the ``case E: t`` tactic work together with + :flag:`Universe Polymorphism` and equality in :g:`Type`. + This makes :tacn:`case <case (ssreflect)>` compatible with the HoTT + library https://github.com/HoTT/HoTT + (`#10302 <https://github.com/coq/coq/pull/10302>`_, + fixes `#10301 <https://github.com/coq/coq/issues/10301>`_, + by Andreas Lynge, review by Enrico Tassi) +- Make the ``rewrite /t`` tactic work together with + :flag:`Universe Polymorphism`. + This makes :tacn:`rewrite <rewrite (ssreflect)>` compatible with the HoTT + library https://github.com/HoTT/HoTT + (`#10305 <https://github.com/coq/coq/pull/10305>`_, + fixes `#9336 <https://github.com/coq/coq/issues/9336>`_, + by Andreas Lynge, review by Enrico Tassi) + +**CoqIDE** + +- Fix CoqIDE instability on Windows after the update to gtk3 + (`#10360 <https://github.com/coq/coq/pull/10360>`_, by Michael Soegtrop, + closes `#9885 <https://github.com/coq/coq/issues/9885>`_). + +**Miscellaneous** + +- Proof General can now display Coq-generated diffs between proof steps + in color + (`#10019 <https://github.com/coq/coq/pull/10019>`_ and + (in Proof General) `#421 <https://github.com/ProofGeneral/PG/pull/421>`_, + by Jim Fehrle). + + Version 8.9 ----------- @@ -957,6 +1011,19 @@ Notations refer to `app`. Solution: wrap `_ ++ _` in `(_ ++ _)%list` (or whichever scope you want). +Changes in 8.8.0 +~~~~~~~~~~~~~~~~ + +Various bug fixes. + +Changes in 8.8.1 +~~~~~~~~~~~~~~~~ + +- Some quality-of-life fixes. +- Numerous improvements to the documentation. +- Fix a critical bug related to primitive projections and :tacn:`native_compute`. +- Ship several additional Coq libraries with the Windows installer. + Version 8.8 ----------- diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py index 53309cd313..867a19efe5 100755 --- a/doc/sphinx/conf.py +++ b/doc/sphinx/conf.py @@ -1,8 +1,7 @@ #!/usr/bin/env python3 -# -*- coding: utf-8 -*- ########################################################################## ## # The Coq Proof Assistant / The Coq Development Team ## -## v # INRIA, CNRS and contributors - Copyright 1999-2018 ## +## v # INRIA, CNRS and contributors - Copyright 1999-2019 ## ## <O___,, # (see CREDITS file for the list of authors) ## ## \VV/ ############################################################### ## // # This file is distributed under the terms of the ## @@ -109,7 +108,7 @@ master_doc = "index" # General information about the project. project = 'Coq' -copyright = '1999-2018, Inria' +copyright = '1999-2019, Inria, CNRS and contributors' author = 'The Coq Development Team' # The version info for the project you're documenting, acts as replacement for diff --git a/doc/sphinx/coqdoc.css b/doc/sphinx/coqdoc.css index a34bb81ebd..2ac2af1c13 100644 --- a/doc/sphinx/coqdoc.css +++ b/doc/sphinx/coqdoc.css @@ -1,6 +1,6 @@ /************************************************************************/ /* * The Coq Proof Assistant / The Coq Development Team */ -/* v * INRIA, CNRS and contributors - Copyright 1999-2018 */ +/* v * INRIA, CNRS and contributors - Copyright 1999-2019 */ /* <O___,, * (see CREDITS file for the list of authors) */ /* \VV/ **************************************************************/ /* // * This file is distributed under the terms of the */ diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst index ebaa6fde66..38f6714f46 100644 --- a/doc/sphinx/language/gallina-specification-language.rst +++ b/doc/sphinx/language/gallina-specification-language.rst @@ -1508,7 +1508,10 @@ the following attributes names are recognized: Takes as value the optional attributes ``since`` and ``note``; both have a string value. - This attribute can trigger the following warnings: + This attribute is supported by the following commands: :cmd:`Ltac`, + :cmd:`Tactic Notation`, :cmd:`Notation`, :cmd:`Infix`. + + It can trigger the following warnings: .. warn:: Tactic @qualid is deprecated since @string. @string. :undocumented: @@ -1516,6 +1519,11 @@ the following attributes names are recognized: .. warn:: Tactic Notation @qualid is deprecated since @string. @string. :undocumented: + .. warn:: Notation @string__1 is deprecated since @string__2. @string__3. + + :n:`@string__1` is the actual notation, :n:`@string__2` is the version number, + :n:`@string__3` is the note. + .. example:: .. coqtop:: all reset warn diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index c48dd5b99e..46f9826e41 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -52,7 +52,7 @@ 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 +The main entry of the grammar is :n:`@ltac_expr`. This language is used in proof mode but it can also be used in toplevel definitions as shown below. .. note:: @@ -89,39 +89,39 @@ mode but it can also be used in toplevel definitions as shown below. :n:`((try (repeat (@tactic__1 || @tactic__2)); @tactic__3); [ {+| @tactic } ]); @tactic__4` .. productionlist:: coq - expr : `expr` ; `expr` - : [> `expr` | ... | `expr` ] - : `expr` ; [ `expr` | ... | `expr` ] - : `tacexpr3` - tacexpr3 : do (`natural` | `ident`) `tacexpr3` - : progress `tacexpr3` - : repeat `tacexpr3` - : try `tacexpr3` - : once `tacexpr3` - : exactly_once `tacexpr3` - : timeout (`natural` | `ident`) `tacexpr3` - : time [`string`] `tacexpr3` - : only `selector`: `tacexpr3` - : `tacexpr2` - tacexpr2 : `tacexpr1` || `tacexpr3` - : `tacexpr1` + `tacexpr3` - : tryif `tacexpr1` then `tacexpr1` else `tacexpr1` - : `tacexpr1` - tacexpr1 : fun `name` ... `name` => `atom` + ltac_expr : `ltac_expr` ; `ltac_expr` + : [> `ltac_expr` | ... | `ltac_expr` ] + : `ltac_expr` ; [ `ltac_expr` | ... | `ltac_expr` ] + : `ltac_expr3` + ltac_expr3 : do (`natural` | `ident`) `ltac_expr3` + : progress `ltac_expr3` + : repeat `ltac_expr3` + : try `ltac_expr3` + : once `ltac_expr3` + : exactly_once `ltac_expr3` + : timeout (`natural` | `ident`) `ltac_expr3` + : time [`string`] `ltac_expr3` + : only `selector`: `ltac_expr3` + : `ltac_expr2` + ltac_expr2 : `ltac_expr1` || `ltac_expr3` + : `ltac_expr1` + `ltac_expr3` + : tryif `ltac_expr1` then `ltac_expr1` else `ltac_expr1` + : `ltac_expr1` + ltac_expr1 : fun `name` ... `name` => `atom` : let [rec] `let_clause` with ... with `let_clause` in `atom` : match goal with `context_rule` | ... | `context_rule` end : match reverse goal with `context_rule` | ... | `context_rule` end - : match `expr` with `match_rule` | ... | `match_rule` end + : match `ltac_expr` with `match_rule` | ... | `match_rule` end : lazymatch goal with `context_rule` | ... | `context_rule` end : lazymatch reverse goal with `context_rule` | ... | `context_rule` end - : lazymatch `expr` with `match_rule` | ... | `match_rule` end + : lazymatch `ltac_expr` with `match_rule` | ... | `match_rule` end : multimatch goal with `context_rule` | ... | `context_rule` end : multimatch reverse goal with `context_rule` | ... | `context_rule` end - : multimatch `expr` with `match_rule` | ... | `match_rule` end + : multimatch `ltac_expr` with `match_rule` | ... | `match_rule` end : abstract `atom` : abstract `atom` using `ident` - : first [ `expr` | ... | `expr` ] - : solve [ `expr` | ... | `expr` ] + : first [ `ltac_expr` | ... | `ltac_expr` ] + : solve [ `ltac_expr` | ... | `ltac_expr` ] : idtac [ `message_token` ... `message_token`] : fail [`natural`] [`message_token` ... `message_token`] : gfail [`natural`] [`message_token` ... `message_token`] @@ -134,31 +134,31 @@ mode but it can also be used in toplevel definitions as shown below. : type_term `term` : numgoals : guard `test` - : assert_fails `tacexpr3` - : assert_succeeds `tacexpr3` + : assert_fails `ltac_expr3` + : assert_succeeds `ltac_expr3` : `tactic` : `qualid` `tacarg` ... `tacarg` : `atom` atom : `qualid` : () : `integer` - : ( `expr` ) + : ( `ltac_expr` ) component : `string` | `qualid` message_token : `string` | `ident` | `integer` tacarg : `qualid` : () : ltac : `atom` : `term` - let_clause : `ident` [`name` ... `name`] := `expr` - context_rule : `context_hyp`, ..., `context_hyp` |- `cpattern` => `expr` - : `cpattern` => `expr` - : |- `cpattern` => `expr` - : _ => `expr` + let_clause : `ident` [`name` ... `name`] := `ltac_expr` + context_rule : `context_hyp`, ..., `context_hyp` |- `cpattern` => `ltac_expr` + : `cpattern` => `ltac_expr` + : |- `cpattern` => `ltac_expr` + : _ => `ltac_expr` context_hyp : `name` : `cpattern` : `name` := `cpattern` [: `cpattern`] - match_rule : `cpattern` => `expr` - : context [`ident`] [ `cpattern` ] => `expr` - : _ => `expr` + match_rule : `cpattern` => `ltac_expr` + : context [`ident`] [ `cpattern` ] => `ltac_expr` + : _ => `ltac_expr` test : `integer` = `integer` : `integer` (< | <= | > | >=) `integer` selector : [`ident`] @@ -171,8 +171,8 @@ mode but it can also be used in toplevel definitions as shown below. .. productionlist:: coq top : [Local] Ltac `ltac_def` with ... with `ltac_def` - ltac_def : `ident` [`ident` ... `ident`] := `expr` - : `qualid` [`ident` ... `ident`] ::= `expr` + ltac_def : `ident` [`ident` ... `ident`] := `ltac_expr` + : `qualid` [`ident` ... `ident`] ::= `ltac_expr` .. _ltac-semantics: @@ -197,12 +197,12 @@ Sequence A sequence is an expression of the following form: -.. tacn:: @expr__1 ; @expr__2 +.. tacn:: @ltac_expr__1 ; @ltac_expr__2 :name: ltac-seq - The expression :n:`@expr__1` is evaluated to :n:`v__1`, which must be + The expression :n:`@ltac_expr__1` is evaluated to :n:`v__1`, which must be a tactic value. The tactic :n:`v__1` is applied to the current goal, - possibly producing more goals. Then :n:`@expr__2` is evaluated to + possibly producing more goals. Then :n:`@ltac_expr__2` is evaluated to produce :n:`v__2`, which must be a tactic value. The tactic :n:`v__2` is applied to all the goals produced by the prior application. Sequence is associative. @@ -213,10 +213,10 @@ Local application of tactics Different tactics can be applied to the different goals using the following form: -.. tacn:: [> {*| @expr }] +.. tacn:: [> {*| @ltac_expr }] :name: [> ... | ... | ... ] (dispatch) - The expressions :n:`@expr__i` are evaluated to :n:`v__i`, for + The expressions :n:`@ltac_expr__i` are evaluated to :n:`v__i`, for i = 1, ..., n and all have to be tactics. The :n:`v__i` is applied to the i-th goal, for i = 1, ..., n. It fails if the number of focused goals is not exactly n. @@ -227,31 +227,31 @@ following form: were given. For instance, ``[> | auto]`` is a shortcut for ``[> idtac | auto ]``. - .. tacv:: [> {*| @expr__i} | @expr .. | {*| @expr__j}] + .. tacv:: [> {*| @ltac_expr__i} | @ltac_expr .. | {*| @ltac_expr__j}] - In this variant, :n:`@expr` is used for each goal coming after those - covered by the list of :n:`@expr__i` but before those covered by the - list of :n:`@expr__j`. + In this variant, :n:`@ltac_expr` is used for each goal coming after those + covered by the list of :n:`@ltac_expr__i` but before those covered by the + list of :n:`@ltac_expr__j`. - .. tacv:: [> {*| @expr} | .. | {*| @expr}] + .. tacv:: [> {*| @ltac_expr} | .. | {*| @ltac_expr}] In this variant, idtac is used for the goals not covered by the two lists of - :n:`@expr`. + :n:`@ltac_expr`. - .. tacv:: [> @expr .. ] + .. tacv:: [> @ltac_expr .. ] - In this variant, the tactic :n:`@expr` is applied independently to each of + In this variant, the tactic :n:`@ltac_expr` is applied independently to each of the goals, rather than globally. In particular, if there are no goals, the tactic is not run at all. A tactic which expects multiple goals, such as ``swap``, would act as if a single goal is focused. - .. tacv:: @expr__0 ; [{*| @expr__i}] + .. tacv:: @ltac_expr__0 ; [{*| @ltac_expr__i}] This variant of local tactic application is paired with a sequence. In this - variant, there must be as many :n:`@expr__i` as goals generated - by the application of :n:`@expr__0` to each of the individual goals + variant, there must be as many :n:`@ltac_expr__i` as goals generated + by the application of :n:`@ltac_expr__0` to each of the individual goals independently. All the above variants work in this form too. - Formally, :n:`@expr ; [ ... ]` is equivalent to :n:`[> @expr ; [> ... ] .. ]`. + Formally, :n:`@ltac_expr ; [ ... ]` is equivalent to :n:`[> @ltac_expr ; [> ... ] .. ]`. .. _goal-selectors: @@ -261,53 +261,53 @@ Goal selectors We can restrict the application of a tactic to a subset of the currently focused goals with: -.. tacn:: @toplevel_selector : @expr +.. tacn:: @toplevel_selector : @ltac_expr :name: ... : ... (goal selector) We can also use selectors as a tactical, which allows to use them nested in a tactic expression, by using the keyword ``only``: - .. tacv:: only @selector : @expr + .. tacv:: only @selector : @ltac_expr :name: only ... : ... - When selecting several goals, the tactic :token:`expr` is applied globally to all + When selecting several goals, the tactic :token:`ltac_expr` is applied globally to all selected goals. - .. tacv:: [@ident] : @expr + .. tacv:: [@ident] : @ltac_expr - In this variant, :token:`expr` is applied locally to a goal previously named + In this variant, :token:`ltac_expr` is applied locally to a goal previously named by the user (see :ref:`existential-variables`). - .. tacv:: @num : @expr + .. tacv:: @num : @ltac_expr - In this variant, :token:`expr` is applied locally to the :token:`num`-th goal. + In this variant, :token:`ltac_expr` is applied locally to the :token:`num`-th goal. - .. tacv:: {+, @num-@num} : @expr + .. tacv:: {+, @num-@num} : @ltac_expr - In this variant, :n:`@expr` is applied globally to the subset of goals + In this variant, :n:`@ltac_expr` is applied globally to the subset of goals described by the given ranges. You can write a single ``n`` as a shortcut for ``n-n`` when specifying multiple ranges. - .. tacv:: all: @expr + .. tacv:: all: @ltac_expr :name: all: ... - In this variant, :token:`expr` is applied to all focused goals. ``all:`` can only + In this variant, :token:`ltac_expr` is applied to all focused goals. ``all:`` can only be used at the toplevel of a tactic expression. - .. tacv:: !: @expr + .. tacv:: !: @ltac_expr - In this variant, if exactly one goal is focused, :token:`expr` is + In this variant, if exactly one goal is focused, :token:`ltac_expr` is applied to it. Otherwise the tactic fails. ``!:`` can only be used at the toplevel of a tactic expression. - .. tacv:: par: @expr + .. tacv:: par: @ltac_expr :name: par: ... - In this variant, :n:`@expr` is applied to all focused goals in parallel. + In this variant, :n:`@ltac_expr` is applied to all focused goals in parallel. The number of workers can be controlled via the command line option ``-async-proofs-tac-j`` taking as argument the desired number of workers. Limitations: ``par:`` only works on goals containing no existential - variables and :n:`@expr` must either solve the goal completely or do + variables and :n:`@ltac_expr` must either solve the goal completely or do nothing (i.e. it cannot make some progress). ``par:`` can only be used at the toplevel of a tactic expression. @@ -322,10 +322,10 @@ For loop There is a for loop that repeats a tactic :token:`num` times: -.. tacn:: do @num @expr +.. tacn:: do @num @ltac_expr :name: do - :n:`@expr` is evaluated to ``v`` which must be a tactic value. This tactic + :n:`@ltac_expr` is evaluated to ``v`` which must be a tactic value. This tactic value ``v`` is applied :token:`num` times. Supposing :token:`num` > 1, after the first application of ``v``, ``v`` is applied, at least once, to the generated subgoals and so on. It fails if the application of ``v`` fails before the num @@ -336,24 +336,24 @@ Repeat loop We have a repeat loop with: -.. tacn:: repeat @expr +.. tacn:: repeat @ltac_expr :name: repeat - :n:`@expr` is evaluated to ``v``. If ``v`` denotes a tactic, this tactic is + :n:`@ltac_expr` is evaluated to ``v``. If ``v`` denotes a tactic, this tactic is applied to each focused goal independently. If the application succeeds, the tactic is applied recursively to all the generated subgoals until it eventually fails. The recursion stops in a subgoal when the tactic has failed *to make - progress*. The tactic :n:`repeat @expr` itself never fails. + progress*. The tactic :n:`repeat @ltac_expr` itself never fails. Error catching ~~~~~~~~~~~~~~ We can catch the tactic errors with: -.. tacn:: try @expr +.. tacn:: try @ltac_expr :name: try - :n:`@expr` is evaluated to ``v`` which must be a tactic value. The tactic + :n:`@ltac_expr` is evaluated to ``v`` which must be a tactic value. The tactic value ``v`` is applied to each focused goal independently. If the application of ``v`` fails in a goal, it catches the error and leaves the goal unchanged. If the level of the exception is positive, then the exception is re-raised with its @@ -364,10 +364,10 @@ Detecting progress We can check if a tactic made progress with: -.. tacn:: progress @expr +.. tacn:: progress @ltac_expr :name: progress - :n:`@expr` is evaluated to v which must be a tactic value. The tactic value ``v`` + :n:`@ltac_expr` is evaluated to v which must be a tactic value. The tactic value ``v`` is applied to each focued subgoal independently. If the application of ``v`` to one of the focused subgoal produced subgoals equal to the initial goals (up to syntactical equality), then an error of level 0 is raised. @@ -380,19 +380,19 @@ Backtracking branching We can branch with the following structure: -.. tacn:: @expr__1 + @expr__2 +.. tacn:: @ltac_expr__1 + @ltac_expr__2 :name: + (backtracking branching) - :n:`@expr__1` and :n:`@expr__2` are evaluated respectively to :n:`v__1` and + :n:`@ltac_expr__1` and :n:`@ltac_expr__2` are evaluated respectively to :n:`v__1` and :n:`v__2` which must be tactic values. The tactic value :n:`v__1` is applied to each focused goal independently and if it fails or a later tactic fails, then the proof backtracks to the current goal and :n:`v__2` is applied. Tactics can be seen as having several successes. When a tactic fails it asks for more successes of the prior tactics. - :n:`@expr__1 + @expr__2` has all the successes of :n:`v__1` followed by all the + :n:`@ltac_expr__1 + @ltac_expr__2` has all the successes of :n:`v__1` followed by all the successes of :n:`v__2`. Algebraically, - :n:`(@expr__1 + @expr__2); @expr__3 = (@expr__1; @expr__3) + (@expr__2; @expr__3)`. + :n:`(@ltac_expr__1 + @ltac_expr__2); @ltac_expr__3 = (@ltac_expr__1; @ltac_expr__3) + (@ltac_expr__2; @ltac_expr__3)`. Branching is left-associative. @@ -403,22 +403,22 @@ Backtracking branching may be too expensive. In this case we may restrict to a local, left biased, branching and consider the first tactic to work (i.e. which does not fail) among a panel of tactics: -.. tacn:: first [{*| @expr}] +.. tacn:: first [{*| @ltac_expr}] :name: first - The :n:`@expr__i` are evaluated to :n:`v__i` and :n:`v__i` must be + The :n:`@ltac_expr__i` are evaluated to :n:`v__i` and :n:`v__i` must be tactic values for i = 1, ..., n. Supposing n > 1, - :n:`first [@expr__1 | ... | @expr__n]` applies :n:`v__1` in each + :n:`first [@ltac_expr__1 | ... | @ltac_expr__n]` applies :n:`v__1` in each focused goal independently and stops if it succeeds; otherwise it tries to apply :n:`v__2` and so on. It fails when there is no applicable tactic. In other words, - :n:`first [@expr__1 | ... | @expr__n]` behaves, in each goal, as the first + :n:`first [@ltac_expr__1 | ... | @ltac_expr__n]` behaves, in each goal, as the first :n:`v__i` to have *at least* one success. .. exn:: No applicable tactic. :undocumented: - .. tacv:: first @expr + .. tacv:: first @ltac_expr This is an |Ltac| alias that gives a primitive access to the first tactical as an |Ltac| definition without going through a parsing rule. It @@ -437,14 +437,14 @@ Left-biased branching Yet another way of branching without backtracking is the following structure: -.. tacn:: @expr__1 || @expr__2 +.. tacn:: @ltac_expr__1 || @ltac_expr__2 :name: || (left-biased branching) - :n:`@expr__1` and :n:`@expr__2` are evaluated respectively to :n:`v__1` and + :n:`@ltac_expr__1` and :n:`@ltac_expr__2` are evaluated respectively to :n:`v__1` and :n:`v__2` which must be tactic values. The tactic value :n:`v__1` is applied in each subgoal independently and if it fails *to progress* then - :n:`v__2` is applied. :n:`@expr__1 || @expr__2` is - equivalent to :n:`first [ progress @expr__1 | @expr__2 ]` (except that + :n:`v__2` is applied. :n:`@ltac_expr__1 || @ltac_expr__2` is + equivalent to :n:`first [ progress @ltac_expr__1 | @ltac_expr__2 ]` (except that if it fails, it fails like :n:`v__2`). Branching is left-associative. Generalized biased branching @@ -452,19 +452,19 @@ Generalized biased branching The tactic -.. tacn:: tryif @expr__1 then @expr__2 else @expr__3 +.. tacn:: tryif @ltac_expr__1 then @ltac_expr__2 else @ltac_expr__3 :name: tryif is a generalization of the biased-branching tactics above. The - expression :n:`@expr__1` is evaluated to :n:`v__1`, which is then + expression :n:`@ltac_expr__1` is evaluated to :n:`v__1`, which is then applied to each subgoal independently. For each goal where :n:`v__1` - succeeds at least once, :n:`@expr__2` is evaluated to :n:`v__2` which + succeeds at least once, :n:`@ltac_expr__2` is evaluated to :n:`v__2` which is then applied collectively to the generated subgoals. The :n:`v__2` tactic can trigger backtracking points in :n:`v__1`: where :n:`v__1` succeeds at least once, - :n:`tryif @expr__1 then @expr__2 else @expr__3` is equivalent to + :n:`tryif @ltac_expr__1 then @ltac_expr__2 else @ltac_expr__3` is equivalent to :n:`v__1; v__2`. In each of the goals where :n:`v__1` does not succeed at least - once, :n:`@expr__3` is evaluated in :n:`v__3` which is is then applied to the + once, :n:`@ltac_expr__3` is evaluated in :n:`v__3` which is is then applied to the goal. Soft cut @@ -473,13 +473,13 @@ Soft cut Another way of restricting backtracking is to restrict a tactic to a single success *a posteriori*: -.. tacn:: once @expr +.. tacn:: once @ltac_expr :name: once - :n:`@expr` is evaluated to ``v`` which must be a tactic value. The tactic value + :n:`@ltac_expr` is evaluated to ``v`` which must be a tactic value. The tactic value ``v`` is applied but only its first success is used. If ``v`` fails, - :n:`once @expr` fails like ``v``. If ``v`` has at least one success, - :n:`once @expr` succeeds once, but cannot produce more successes. + :n:`once @ltac_expr` fails like ``v``. If ``v`` has at least one success, + :n:`once @ltac_expr` succeeds once, but cannot produce more successes. Checking the successes ~~~~~~~~~~~~~~~~~~~~~~ @@ -487,14 +487,14 @@ Checking the successes Coq provides an experimental way to check that a tactic has *exactly one* success: -.. tacn:: exactly_once @expr +.. tacn:: exactly_once @ltac_expr :name: exactly_once - :n:`@expr` is evaluated to ``v`` which must be a tactic value. The tactic value + :n:`@ltac_expr` is evaluated to ``v`` which must be a tactic value. The tactic value ``v`` is applied if it has at most one success. If ``v`` fails, - :n:`exactly_once @expr` fails like ``v``. If ``v`` has a exactly one success, - :n:`exactly_once @expr` succeeds like ``v``. If ``v`` has two or more - successes, exactly_once expr fails. + :n:`exactly_once @ltac_expr` fails like ``v``. If ``v`` has a exactly one success, + :n:`exactly_once @ltac_expr` succeeds like ``v``. If ``v`` has two or more + successes, :n:`exactly_once @ltac_expr` fails. .. warning:: @@ -513,10 +513,10 @@ Checking the failure Coq provides a derived tactic to check that a tactic *fails*: -.. tacn:: assert_fails @expr +.. tacn:: assert_fails @ltac_expr :name: assert_fails - This behaves like :n:`tryif @expr then fail 0 tac "succeeds" else idtac`. + This behaves like :n:`tryif @ltac_expr then fail 0 tac "succeeds" else idtac`. Checking the success ~~~~~~~~~~~~~~~~~~~~ @@ -524,7 +524,7 @@ Checking the success Coq provides a derived tactic to check that a tactic has *at least one* success: -.. tacn:: assert_succeeds @expr +.. tacn:: assert_succeeds @ltac_expr :name: assert_succeeds This behaves like @@ -536,19 +536,19 @@ Solving We may consider the first to solve (i.e. which generates no subgoal) among a panel of tactics: -.. tacn:: solve [{*| @expr}] +.. tacn:: solve [{*| @ltac_expr}] :name: solve - The :n:`@expr__i` are evaluated to :n:`v__i` and :n:`v__i` must be + The :n:`@ltac_expr__i` are evaluated to :n:`v__i` and :n:`v__i` must be tactic values, for i = 1, ..., n. Supposing n > 1, - :n:`solve [@expr__1 | ... | @expr__n]` applies :n:`v__1` to + :n:`solve [@ltac_expr__1 | ... | @ltac_expr__n]` applies :n:`v__1` to each goal independently and stops if it succeeds; otherwise it tries to apply :n:`v__2` and so on. It fails if there is no solving tactic. .. exn:: Cannot solve the goal. :undocumented: - .. tacv:: solve @expr + .. tacv:: solve @ltac_expr This is an |Ltac| alias that gives a primitive access to the :n:`solve:` tactical. See the :n:`first` tactical for more information. @@ -651,10 +651,10 @@ Timeout We can force a tactic to stop if it has not finished after a certain amount of time: -.. tacn:: timeout @num @expr +.. tacn:: timeout @num @ltac_expr :name: timeout - :n:`@expr` is evaluated to ``v`` which must be a tactic value. The tactic value + :n:`@ltac_expr` is evaluated to ``v`` which must be a tactic value. The tactic value ``v`` is applied normally, except that it is interrupted after :n:`@num` seconds if it is still running. In this case the outcome is a failure. @@ -673,10 +673,10 @@ Timing a tactic A tactic execution can be timed: -.. tacn:: time @string @expr +.. tacn:: time @string @ltac_expr :name: time - evaluates :n:`@expr` and displays the running time of the tactic expression, whether it + evaluates :n:`@ltac_expr` and displays the running time of the tactic expression, whether it fails or succeeds. In case of several successes, the time for each successive run is displayed. Time is in seconds and is machine-dependent. The :n:`@string` argument is optional. When provided, it is used to identify this particular @@ -688,10 +688,10 @@ Timing a tactic that evaluates to a term Tactic expressions that produce terms can be timed with the experimental tactic -.. tacn:: time_constr @expr +.. tacn:: time_constr @ltac_expr :name: time_constr - which evaluates :n:`@expr ()` and displays the time the tactic expression + which evaluates :n:`@ltac_expr ()` and displays the time the tactic expression evaluated, assuming successful evaluation. Time is in seconds and is machine-dependent. @@ -739,12 +739,12 @@ Local definitions Local definitions can be done as follows: -.. tacn:: let @ident__1 := @expr__1 {* with @ident__i := @expr__i} in @expr +.. tacn:: let @ident__1 := @ltac_expr__1 {* with @ident__i := @ltac_expr__i} in @ltac_expr :name: let ... := ... - each :n:`@expr__i` is evaluated to :n:`v__i`, then, :n:`@expr` is evaluated + each :n:`@ltac_expr__i` is evaluated to :n:`v__i`, then, :n:`@ltac_expr` is evaluated by substituting :n:`v__i` to each occurrence of :n:`@ident__i`, for - i = 1, ..., n. There are no dependencies between the :n:`@expr__i` and the + i = 1, ..., n. There are no dependencies between the :n:`@ltac_expr__i` and the :n:`@ident__i`. Local definitions can be made recursive by using :n:`let rec` instead of :n:`let`. @@ -763,7 +763,7 @@ An application is an expression of the following form: The reference :n:`@qualid` must be bound to some defined tactic definition expecting at least as many arguments as the provided :n:`tacarg`. The - expressions :n:`@expr__i` are evaluated to :n:`v__i`, for i = 1, ..., n. + expressions :n:`@ltac_expr__i` are evaluated to :n:`v__i`, for i = 1, ..., n. .. what expressions ?? @@ -773,7 +773,7 @@ Function construction A parameterized tactic can be built anonymously (without resorting to local definitions) with: -.. tacn:: fun {+ @ident} => @expr +.. tacn:: fun {+ @ident} => @ltac_expr Indeed, local definitions of functions are a syntactic sugar for binding a :n:`fun` tactic to an identifier. @@ -783,9 +783,9 @@ Pattern matching on terms We can carry out pattern matching on terms with: -.. tacn:: match @expr with {+| @cpattern__i => @expr__i} end +.. tacn:: match @ltac_expr with {+| @cpattern__i => @ltac_expr__i} end - The expression :n:`@expr` is evaluated and should yield a term which is + The expression :n:`@ltac_expr` is evaluated and should yield a term which is matched against :n:`cpattern__1`. The matching is non-linear: if a metavariable occurs more than once, it should match the same expression every time. It is first-order except on the variables of the form :n:`@?id` @@ -799,20 +799,20 @@ We can carry out pattern matching on terms with: same types. This provides with a primitive form of matching under context which does not require manipulating a functional term. - If the matching with :n:`@cpattern__1` succeeds, then :n:`@expr__1` is + If the matching with :n:`@cpattern__1` succeeds, then :n:`@ltac_expr__1` is evaluated into some value by substituting the pattern matching - instantiations to the metavariables. If :n:`@expr__1` evaluates to a + instantiations to the metavariables. If :n:`@ltac_expr__1` evaluates to a tactic and the match expression is in position to be applied to a goal (e.g. it is not bound to a variable by a :n:`let in`), then this tactic is applied. If the tactic succeeds, the list of resulting subgoals is the - result of the match expression. If :n:`@expr__1` does not evaluate to a + result of the match expression. If :n:`@ltac_expr__1` does not evaluate to a tactic or if the match expression is not in position to be applied to a - goal, then the result of the evaluation of :n:`@expr__1` is the result + goal, then the result of the evaluation of :n:`@ltac_expr__1` is the result of the match expression. If the matching with :n:`@cpattern__1` fails, or if it succeeds but the - evaluation of :n:`@expr__1` fails, or if the evaluation of - :n:`@expr__1` succeeds but returns a tactic in execution position whose + evaluation of :n:`@ltac_expr__1` fails, or if the evaluation of + :n:`@ltac_expr__1` succeeds but returns a tactic in execution position whose execution fails, then :n:`cpattern__2` is used and so on. The pattern :n:`_` matches any term and shadows all remaining patterns if any. If all clauses fail (in particular, there is no pattern :n:`_`) then a @@ -828,9 +828,9 @@ We can carry out pattern matching on terms with: .. exn:: Argument of match does not evaluate to a term. - This happens when :n:`@expr` does not denote a term. + This happens when :n:`@ltac_expr` does not denote a term. - .. tacv:: multimatch @expr with {+| @cpattern__i => @expr__i} end + .. tacv:: multimatch @ltac_expr with {+| @cpattern__i => @ltac_expr__i} end Using multimatch instead of match will allow subsequent tactics to backtrack into a right-hand side tactic which has backtracking points @@ -839,7 +839,7 @@ We can carry out pattern matching on terms with: The syntax :n:`match …` is, in fact, a shorthand for :n:`once multimatch …`. - .. tacv:: lazymatch @expr with {+| @cpattern__i => @expr__i} end + .. tacv:: lazymatch @ltac_expr with {+| @cpattern__i => @ltac_expr__i} end Using lazymatch instead of match will perform the same pattern matching procedure but will commit to the first matching branch @@ -884,13 +884,13 @@ We can perform pattern matching on goals using the following expression: .. we should provide the full grammar here -.. tacn:: match goal with {+| {+, @context_hyp} |- @cpattern => @expr } | _ => @expr end +.. tacn:: match goal with {+| {+, @context_hyp} |- @cpattern => @ltac_expr } | _ => @ltac_expr end :name: match goal If each hypothesis pattern :n:`hyp`\ :sub:`1,i`, with i = 1, ..., m\ :sub:`1` is matched (non-linear first-order unification) by a hypothesis of the goal and if :n:`cpattern_1` is matched by the conclusion of the goal, - then :n:`@expr__1` is evaluated to :n:`v__1` by substituting the + then :n:`@ltac_expr__1` is evaluated to :n:`v__1` by substituting the pattern matching to the metavariables and the real hypothesis names bound to the possible hypothesis names occurring in the hypothesis patterns. If :n:`v__1` is a tactic value, then it is applied to the @@ -898,7 +898,7 @@ We can perform pattern matching on goals using the following expression: is tried with the same proof context pattern. If there is no other combination of hypotheses then the second proof context pattern is tried and so on. If the next to last proof context pattern fails then - the last :n:`@expr` is evaluated to :n:`v` and :n:`v` is + the last :n:`@ltac_expr` is evaluated to :n:`v` and :n:`v` is applied. Note also that matching against subterms (using the :n:`context @ident [ @cpattern ]`) is available and is also subject to yielding several matchings. @@ -922,7 +922,7 @@ We can perform pattern matching on goals using the following expression: first), but it possible to reverse this order (oldest first) with the :n:`match reverse goal with` variant. - .. tacv:: multimatch goal with {+| {+, @context_hyp} |- @cpattern => @expr } | _ => @expr end + .. tacv:: multimatch goal with {+| {+, @context_hyp} |- @cpattern => @ltac_expr } | _ => @ltac_expr end Using :n:`multimatch` instead of :n:`match` will allow subsequent tactics to backtrack into a right-hand side tactic which has backtracking points @@ -933,7 +933,7 @@ We can perform pattern matching on goals using the following expression: The syntax :n:`match [reverse] goal …` is, in fact, a shorthand for :n:`once multimatch [reverse] goal …`. - .. tacv:: lazymatch goal with {+| {+, @context_hyp} |- @cpattern => @expr } | _ => @expr end + .. tacv:: lazymatch goal with {+| {+, @context_hyp} |- @cpattern => @ltac_expr } | _ => @ltac_expr end Using lazymatch instead of match will perform the same pattern matching procedure but will commit to the first matching branch with the first @@ -948,11 +948,11 @@ Filling a term context The following expression is not a tactic in the sense that it does not produce subgoals but generates a term to be used in tactic expressions: -.. tacn:: context @ident [@expr] +.. tacn:: context @ident [@ltac_expr] :n:`@ident` must denote a context variable bound by a context pattern of a match expression. This expression evaluates replaces the hole of the - value of :n:`@ident` by the value of :n:`@expr`. + value of :n:`@ident` by the value of :n:`@ltac_expr`. .. exn:: Not a context variable. :undocumented: @@ -1072,10 +1072,10 @@ Testing boolean expressions Proving a subgoal as a separate lemma ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -.. tacn:: abstract @expr +.. tacn:: abstract @ltac_expr :name: abstract - From the outside, :n:`abstract @expr` is the same as :n:`solve @expr`. + From the outside, :n:`abstract @ltac_expr` is the same as :n:`solve @ltac_expr`. Internally it saves an auxiliary lemma called ``ident_subproofn`` where ``ident`` is the name of the current goal and ``n`` is chosen so that this is a fresh name. Such an auxiliary lemma is inlined in the final proof term. @@ -1098,7 +1098,7 @@ Proving a subgoal as a separate lemma if used as part of typeclass resolution, it may produce wrong terms when in universe polymorphic mode. - .. tacv:: abstract @expr using @ident + .. tacv:: abstract @ltac_expr using @ident Give explicitly the name of the auxiliary lemma. @@ -1107,7 +1107,7 @@ Proving a subgoal as a separate lemma Use this feature at your own risk; explicitly named and reused subterms don’t play well with asynchronous proofs. - .. tacv:: transparent_abstract @expr + .. tacv:: transparent_abstract @ltac_expr :name: transparent_abstract Save the subproof in a transparent lemma rather than an opaque one. @@ -1117,7 +1117,7 @@ Proving a subgoal as a separate lemma Use this feature at your own risk; building computationally relevant terms with tactics is fragile. - .. tacv:: transparent_abstract @expr using @ident + .. tacv:: transparent_abstract @ltac_expr using @ident Give explicitly the name of the auxiliary transparent lemma. @@ -1139,7 +1139,7 @@ Defining |Ltac| functions Basically, |Ltac| toplevel definitions are made as follows: -.. cmd:: {? Local} Ltac @ident {* @ident} := @expr +.. cmd:: {? Local} Ltac @ident {* @ident} := @ltac_expr :name: Ltac This defines a new |Ltac| function that can be used in any tactic @@ -1152,13 +1152,13 @@ Basically, |Ltac| toplevel definitions are made as follows: The preceding definition can equivalently be written: - :n:`Ltac @ident := fun {+ @ident} => @expr` + :n:`Ltac @ident := fun {+ @ident} => @ltac_expr` - .. cmdv:: Ltac @ident {* @ident} {* with @ident {* @ident}} := @expr + .. cmdv:: Ltac @ident {* @ident} {* with @ident {* @ident}} := @ltac_expr This syntax allows recursive and mutual recursive function definitions. - .. cmdv:: Ltac @qualid {* @ident} ::= @expr + .. cmdv:: Ltac @qualid {* @ident} ::= @ltac_expr This syntax *redefines* an existing user-defined tactic. @@ -1585,7 +1585,7 @@ Backtraces Info trace ~~~~~~~~~~ -.. cmd:: Info @num @expr +.. cmd:: Info @num @ltac_expr :name: Info This command can be used to print the trace of the path eventually taken by an diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst index 36eeff6192..3036648b08 100644 --- a/doc/sphinx/proof-engine/ltac2.rst +++ b/doc/sphinx/proof-engine/ltac2.rst @@ -850,8 +850,17 @@ a Ltac1 expression, and semantics of this quotation is the evaluation of the corresponding code for its side effects. In particular, it cannot return values, and the quotation has type :n:`unit`. -Beware, Ltac1 **cannot** access variables from the Ltac2 scope. One is limited -to the use of standalone function calls. +Ltac1 **cannot** implicitly access variables from the Ltac2 scope, but this can +be done via an explicit annotation to the :n:`ltac1` quotation. + +.. productionlist:: coq + ltac2_term : ltac1 : ( `ident` ... `ident` |- `ltac_expr` ) + +The return type of this expression is a function of the same arity as the number +of identifiers, with arguments of type `Ltac2.Ltac1.t` (see below). This syntax +will bind the variables in the quoted Ltac1 code as if they had been bound from +Ltac1 itself. Similarly, the arguments applied to the quotation will be passed +at runtime to the Ltac1 code. Low-level API +++++++++++++ @@ -869,6 +878,9 @@ focus is very hard. This is why some functions return a continuation-passing style value, as it can dispatch dynamically between focused and unfocused behaviour. +The same mechanism for explicit binding of variables as described in the +previous section applies. + Ltac2 from Ltac1 ~~~~~~~~~~~~~~~~ diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst index 0cff987a27..03b30d5d97 100644 --- a/doc/sphinx/proof-engine/proof-handling.rst +++ b/doc/sphinx/proof-engine/proof-handling.rst @@ -600,6 +600,14 @@ Requesting information its normalized form at the current stage of the proof, useful for debugging universe inconsistencies. + .. cmdv:: Show Goal @num at @num + :name: Show Goal + + This command is only available in coqtop. Displays a goal at a + proof state using the goal ID number and the proof state ID number. + It is primarily for use by tools such as Prooftree that need to fetch + goal history in this way. Prooftree is a tool for visualizing a proof + as a tree that runs in Proof General. .. cmd:: Guarded diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 9b381cb9de..fd315c097d 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -1716,9 +1716,9 @@ Tactic notations allow to customize the syntax of tactics. They have the followi - intro * - ``simple_intropattern`` - - intro_pattern - - an intro pattern - - intros + - simple_intropattern + - an introduction pattern + - assert as * - ``hyp`` - identifier diff --git a/doc/tools/coqrst/__init__.py b/doc/tools/coqrst/__init__.py index 2dda7d9216..710a90a6f1 100644 --- a/doc/tools/coqrst/__init__.py +++ b/doc/tools/coqrst/__init__.py @@ -1,6 +1,6 @@ ########################################################################## ## # The Coq Proof Assistant / The Coq Development Team ## -## v # INRIA, CNRS and contributors - Copyright 1999-2018 ## +## v # INRIA, CNRS and contributors - Copyright 1999-2019 ## ## <O___,, # (see CREDITS file for the list of authors) ## ## \VV/ ############################################################### ## // # This file is distributed under the terms of the ## diff --git a/doc/tools/coqrst/checkdeps.py b/doc/tools/coqrst/checkdeps.py index 11f95c4e94..91f0a7cb1b 100644 --- a/doc/tools/coqrst/checkdeps.py +++ b/doc/tools/coqrst/checkdeps.py @@ -1,6 +1,6 @@ ########################################################################## ## # The Coq Proof Assistant / The Coq Development Team ## -## v # INRIA, CNRS and contributors - Copyright 1999-2018 ## +## v # INRIA, CNRS and contributors - Copyright 1999-2019 ## ## <O___,, # (see CREDITS file for the list of authors) ## ## \VV/ ############################################################### ## // # This file is distributed under the terms of the ## diff --git a/doc/tools/coqrst/coqdoc/__init__.py b/doc/tools/coqrst/coqdoc/__init__.py index a89a548e2c..8d19924df1 100644 --- a/doc/tools/coqrst/coqdoc/__init__.py +++ b/doc/tools/coqrst/coqdoc/__init__.py @@ -1,6 +1,6 @@ ########################################################################## ## # The Coq Proof Assistant / The Coq Development Team ## -## v # INRIA, CNRS and contributors - Copyright 1999-2018 ## +## v # INRIA, CNRS and contributors - Copyright 1999-2019 ## ## <O___,, # (see CREDITS file for the list of authors) ## ## \VV/ ############################################################### ## // # This file is distributed under the terms of the ## diff --git a/doc/tools/coqrst/coqdoc/main.py b/doc/tools/coqrst/coqdoc/main.py index ba58ff0084..adacba97cc 100644 --- a/doc/tools/coqrst/coqdoc/main.py +++ b/doc/tools/coqrst/coqdoc/main.py @@ -1,6 +1,6 @@ ########################################################################## ## # The Coq Proof Assistant / The Coq Development Team ## -## v # INRIA, CNRS and contributors - Copyright 1999-2018 ## +## v # INRIA, CNRS and contributors - Copyright 1999-2019 ## ## <O___,, # (see CREDITS file for the list of authors) ## ## \VV/ ############################################################### ## // # This file is distributed under the terms of the ## diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py index 4bdfac7c42..6c32a4968c 100644 --- a/doc/tools/coqrst/coqdomain.py +++ b/doc/tools/coqrst/coqdomain.py @@ -1,7 +1,6 @@ -# -*- coding: utf-8 -*- ########################################################################## ## # The Coq Proof Assistant / The Coq Development Team ## -## v # INRIA, CNRS and contributors - Copyright 1999-2018 ## +## v # INRIA, CNRS and contributors - Copyright 1999-2019 ## ## <O___,, # (see CREDITS file for the list of authors) ## ## \VV/ ############################################################### ## // # This file is distributed under the terms of the ## diff --git a/doc/tools/coqrst/notations/Makefile b/doc/tools/coqrst/notations/Makefile index c017aed951..29132f1cd7 100644 --- a/doc/tools/coqrst/notations/Makefile +++ b/doc/tools/coqrst/notations/Makefile @@ -1,6 +1,6 @@ ########################################################################## ## # The Coq Proof Assistant / The Coq Development Team ## -## v # INRIA, CNRS and contributors - Copyright 1999-2018 ## +## v # INRIA, CNRS and contributors - Copyright 1999-2019 ## ## <O___,, # (see CREDITS file for the list of authors) ## ## \VV/ ############################################################### ## // # This file is distributed under the terms of the ## diff --git a/doc/tools/coqrst/notations/TacticNotations.g b/doc/tools/coqrst/notations/TacticNotations.g index 01c656eb23..905b52525a 100644 --- a/doc/tools/coqrst/notations/TacticNotations.g +++ b/doc/tools/coqrst/notations/TacticNotations.g @@ -1,6 +1,6 @@ /************************************************************************/ /* * The Coq Proof Assistant / The Coq Development Team */ -/* v * INRIA, CNRS and contributors - Copyright 1999-2018 */ +/* v * INRIA, CNRS and contributors - Copyright 1999-2019 */ /* <O___,, * (see CREDITS file for the list of authors) */ /* \VV/ **************************************************************/ /* // * This file is distributed under the terms of the */ diff --git a/doc/tools/coqrst/notations/fontsupport.py b/doc/tools/coqrst/notations/fontsupport.py index a3efd97f5b..f0df7f1c01 100755 --- a/doc/tools/coqrst/notations/fontsupport.py +++ b/doc/tools/coqrst/notations/fontsupport.py @@ -1,8 +1,7 @@ #!/usr/bin/env python2 -# -*- coding: utf-8 -*- ########################################################################## ## # The Coq Proof Assistant / The Coq Development Team ## -## v # INRIA, CNRS and contributors - Copyright 1999-2018 ## +## v # INRIA, CNRS and contributors - Copyright 1999-2019 ## ## <O___,, # (see CREDITS file for the list of authors) ## ## \VV/ ############################################################### ## // # This file is distributed under the terms of the ## @@ -12,6 +11,9 @@ """Transform a font to center each of its characters in square bounding boxes. See https://stackoverflow.com/questions/37377476/ for background information. + +This script is here for reference. It was used to generate the modified +font CoqNotations.ttf from UbuntuMono-B.ttf. """ from collections import Counter diff --git a/doc/tools/coqrst/notations/html.py b/doc/tools/coqrst/notations/html.py index d2b5d86b37..d9c5383774 100644 --- a/doc/tools/coqrst/notations/html.py +++ b/doc/tools/coqrst/notations/html.py @@ -1,6 +1,6 @@ ########################################################################## ## # The Coq Proof Assistant / The Coq Development Team ## -## v # INRIA, CNRS and contributors - Copyright 1999-2018 ## +## v # INRIA, CNRS and contributors - Copyright 1999-2019 ## ## <O___,, # (see CREDITS file for the list of authors) ## ## \VV/ ############################################################### ## // # This file is distributed under the terms of the ## diff --git a/doc/tools/coqrst/notations/parsing.py b/doc/tools/coqrst/notations/parsing.py index 2312e09090..7b7febe668 100644 --- a/doc/tools/coqrst/notations/parsing.py +++ b/doc/tools/coqrst/notations/parsing.py @@ -1,6 +1,6 @@ ########################################################################## ## # The Coq Proof Assistant / The Coq Development Team ## -## v # INRIA, CNRS and contributors - Copyright 1999-2018 ## +## v # INRIA, CNRS and contributors - Copyright 1999-2019 ## ## <O___,, # (see CREDITS file for the list of authors) ## ## \VV/ ############################################################### ## // # This file is distributed under the terms of the ## diff --git a/doc/tools/coqrst/notations/plain.py b/doc/tools/coqrst/notations/plain.py index 2180c8e6a5..93a7ec4683 100644 --- a/doc/tools/coqrst/notations/plain.py +++ b/doc/tools/coqrst/notations/plain.py @@ -1,6 +1,6 @@ ########################################################################## ## # The Coq Proof Assistant / The Coq Development Team ## -## v # INRIA, CNRS and contributors - Copyright 1999-2018 ## +## v # INRIA, CNRS and contributors - Copyright 1999-2019 ## ## <O___,, # (see CREDITS file for the list of authors) ## ## \VV/ ############################################################### ## // # This file is distributed under the terms of the ## diff --git a/doc/tools/coqrst/notations/regexp.py b/doc/tools/coqrst/notations/regexp.py index ea820c719e..697201a5d5 100644 --- a/doc/tools/coqrst/notations/regexp.py +++ b/doc/tools/coqrst/notations/regexp.py @@ -1,6 +1,6 @@ ########################################################################## ## # The Coq Proof Assistant / The Coq Development Team ## -## v # INRIA, CNRS and contributors - Copyright 1999-2018 ## +## v # INRIA, CNRS and contributors - Copyright 1999-2019 ## ## <O___,, # (see CREDITS file for the list of authors) ## ## \VV/ ############################################################### ## // # This file is distributed under the terms of the ## diff --git a/doc/tools/coqrst/notations/sphinx.py b/doc/tools/coqrst/notations/sphinx.py index 4ed09e04a9..4ca0a2ef83 100644 --- a/doc/tools/coqrst/notations/sphinx.py +++ b/doc/tools/coqrst/notations/sphinx.py @@ -1,6 +1,6 @@ ########################################################################## ## # The Coq Proof Assistant / The Coq Development Team ## -## v # INRIA, CNRS and contributors - Copyright 1999-2018 ## +## v # INRIA, CNRS and contributors - Copyright 1999-2019 ## ## <O___,, # (see CREDITS file for the list of authors) ## ## \VV/ ############################################################### ## // # This file is distributed under the terms of the ## diff --git a/doc/tools/coqrst/repl/ansicolors.py b/doc/tools/coqrst/repl/ansicolors.py index 495eea9107..6d9c79d16c 100644 --- a/doc/tools/coqrst/repl/ansicolors.py +++ b/doc/tools/coqrst/repl/ansicolors.py @@ -1,6 +1,6 @@ ########################################################################## ## # The Coq Proof Assistant / The Coq Development Team ## -## v # INRIA, CNRS and contributors - Copyright 1999-2018 ## +## v # INRIA, CNRS and contributors - Copyright 1999-2019 ## ## <O___,, # (see CREDITS file for the list of authors) ## ## \VV/ ############################################################### ## // # This file is distributed under the terms of the ## diff --git a/doc/tools/coqrst/repl/coqtop.py b/doc/tools/coqrst/repl/coqtop.py index 2b124ee5c1..3dc20db82b 100644 --- a/doc/tools/coqrst/repl/coqtop.py +++ b/doc/tools/coqrst/repl/coqtop.py @@ -1,6 +1,6 @@ ########################################################################## ## # The Coq Proof Assistant / The Coq Development Team ## -## v # INRIA, CNRS and contributors - Copyright 1999-2018 ## +## v # INRIA, CNRS and contributors - Copyright 1999-2019 ## ## <O___,, # (see CREDITS file for the list of authors) ## ## \VV/ ############################################################### ## // # This file is distributed under the terms of the ## |