diff options
Diffstat (limited to 'doc')
50 files changed, 924 insertions, 475 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/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/06-ssreflect/10302-case-HoTT.rst b/doc/changelog/06-ssreflect/10302-case-HoTT.rst deleted file mode 100644 index 686b3c3cca..0000000000 --- a/doc/changelog/06-ssreflect/10302-case-HoTT.rst +++ /dev/null @@ -1,7 +0,0 @@ -- Make the ``case E: t`` tactic work together with - :flag:`Universe Polymorphism` and equality in :g:`Type`. - This makes tacn:`case` 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) diff --git a/doc/changelog/06-ssreflect/10305-unfold-HoTT.rst b/doc/changelog/06-ssreflect/10305-unfold-HoTT.rst deleted file mode 100644 index b82de1a879..0000000000 --- a/doc/changelog/06-ssreflect/10305-unfold-HoTT.rst +++ /dev/null @@ -1,7 +0,0 @@ -- Make the ``rewrite /t`` tactic work together with - :flag:`Universe Polymorphism`. - This makes tacn:`rewrite` 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) diff --git a/doc/changelog/09-coqide/10360-windows.rst b/doc/changelog/09-coqide/10360-windows.rst deleted file mode 100644 index b7f8374c73..0000000000 --- a/doc/changelog/09-coqide/10360-windows.rst +++ /dev/null @@ -1,3 +0,0 @@ -- 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>`_). 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_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/changes.rst b/doc/sphinx/changes.rst index 6ff15e52a3..fd84868a1f 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -604,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 ----------- 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/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 cc983565ff..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 ## 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 ## |