aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--.github/CODEOWNERS15
-rw-r--r--.gitlab-ci.yml38
-rw-r--r--.travis.yml32
-rw-r--r--Makefile.build2
-rw-r--r--configure.ml5
-rwxr-xr-xdev/tools/check-overlays.sh4
-rw-r--r--doc/sphinx/credits.rst101
-rw-r--r--doc/sphinx/introduction.rst4
-rw-r--r--kernel/retroknowledge.ml19
-rw-r--r--kernel/retroknowledge.mli20
-rw-r--r--plugins/ltac/extraargs.ml439
11 files changed, 65 insertions, 214 deletions
diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS
index 192a2b181..bbd2d349c 100644
--- a/.github/CODEOWNERS
+++ b/.github/CODEOWNERS
@@ -8,22 +8,15 @@
########## CI infrastructure ##########
-/dev/ci/ @ejgallego
-# Secondary maintainer @SkySkimmer
+/dev/ci/ @coq/ci-maintainers
+/.circleci/ @coq/ci-maintainers
+/.travis.yml @coq/ci-maintainers
+/.gitlab-ci.yml @coq/ci-maintainers
/dev/ci/user-overlays/*.sh @ghost
# Trick to avoid getting review requests
# each time someone adds an overlay
-/.circleci/ @SkySkimmer
-# Secondary maintainer @ejgallego
-
-/.travis.yml @ejgallego
-# Secondary maintainer @SkySkimmer
-
-/.gitlab-ci.yml @SkySkimmer
-# Secondary maintainer @ejgallego
-
/appveyor.yml @maximedenes
/dev/ci/appveyor.* @maximedenes
/dev/ci/*.bat @maximedenes
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 0ad68b508..be19a93a3 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -71,7 +71,7 @@ after_script:
- echo 'end:coq.clean'
- echo 'start:coq.config'
- - ./configure -prefix "$(pwd)/_install_ci" ${COQ_EXTRA_CONF}"$COQ_EXTRA_CONF_QUOTE"
+ - ./configure -warn-error yes -prefix "$(pwd)/_install_ci" ${COQ_EXTRA_CONF}"$COQ_EXTRA_CONF_QUOTE"
- echo 'end:coq.config'
- echo 'start:coq.build'
@@ -88,28 +88,6 @@ after_script:
- set +e
-.warnings-template: &warnings-template
- # keep warnings in test stage so we can test things even when warnings occur
- stage: test
- script:
- - set -e
-
- - echo 'start:coq.clean'
- - make clean # ensure that `make clean` works on a fresh clone
- - echo 'end:coq.clean'
-
- - echo 'start:coq.config'
- - ./configure -local ${COQ_EXTRA_CONF}
- - echo 'end:coq.config'
-
- - echo 'start:coq.build'
- - make -j "$NJOBS" coqocaml
- - echo 'end:coq:build'
-
- - set +e
- variables: &warnings-variables
- COQ_EXTRA_CONF: "-native-compiler yes -coqide byte -byte-only -warn-error yes"
-
# every non build job must set dependencies otherwise all build
# artifacts are used together and we may get some random Coq. To that
# purpose, we add a spurious dependency `not-a-real-job` that must be
@@ -264,20 +242,6 @@ pkg:nix:
paths:
- nix-build-coq.drv-0/*/test-suite/logs
-warnings:base:
- <<: *warnings-template
-
-# warnings:32bit:
-# <<: *warnings-template
-# variables:
-# <<: *warnings-variables
-
-warnings:edge:
- <<: *warnings-template
- variables:
- <<: *warnings-variables
- OPAM_SWITCH: edge
-
documentation:
<<: *doc-template
dependencies:
diff --git a/.travis.yml b/.travis.yml
index 3301d97ce..53fbe5821 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -164,36 +164,6 @@ matrix:
- avsm
packages: *extra-packages
- # Ocaml warnings with two compilers
- - if: NOT (type = pull_request)
- env:
- - MAIN_TARGET="coqocaml"
- - EXTRA_CONF="-byte-only -coqide byte -warn-error yes"
- - EXTRA_OPAM="${LABLGTK}"
- addons:
- apt:
- sources:
- - avsm
- packages: &coqide-packages
- - opam
- - aspcud
- - libgtk2.0-dev
- - libgtksourceview2.0-dev
-
- - if: NOT (type = pull_request)
- env:
- - MAIN_TARGET="coqocaml"
- - COMPILER="${COMPILER_BE}"
- - FINDLIB_VER="${FINDLIB_VER_BE}"
- - CAMLP5_VER="${CAMLP5_VER_BE}"
- - EXTRA_CONF="-byte-only -coqide byte -warn-error yes"
- - EXTRA_OPAM="${LABLGTK_BE}"
- addons:
- apt:
- sources:
- - avsm
- packages: *coqide-packages
-
- os: osx
env:
- TEST_TARGET="test-suite"
@@ -260,7 +230,7 @@ script:
- echo -en 'travis_fold:end:coq.clean\\r'
- echo 'Configuring Coq...' && echo -en 'travis_fold:start:coq.config\\r'
-- ./configure ${COQ_DEST} -native-compiler ${NATIVE_COMP} ${EXTRA_CONF}
+- ./configure ${COQ_DEST} -warn-error yes -native-compiler ${NATIVE_COMP} ${EXTRA_CONF}
- echo -en 'travis_fold:end:coq.config\\r'
- echo 'Building Coq...' && echo -en 'travis_fold:start:coq.build\\r'
diff --git a/Makefile.build b/Makefile.build
index 84f86c99a..c100eda40 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -195,7 +195,7 @@ TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD))
# the output format of the unix command time. For instance:
# TIME="%C (%U user, %S sys, %e total, %M maxres)"
-COQOPTS=$(NATIVECOMPUTE)
+COQOPTS=$(NATIVECOMPUTE) $(COQWARNERROR)
BOOTCOQC=$(TIMER) $(COQTOPBEST) -boot $(COQOPTS) -compile
LOCALINCLUDES=$(addprefix -I ,$(SRCDIRS))
diff --git a/configure.ml b/configure.ml
index 194f47c49..c08e8dfcc 100644
--- a/configure.ml
+++ b/configure.ml
@@ -647,8 +647,10 @@ let camltag = match caml_version_list with
48: implicit elimination of optional arguments: too common
50: unexpected documentation comment: too common and annoying to avoid
56: unreachable match case: the [_ -> .] syntax doesn't exist in 4.02.3
+ 58: "no cmx file was found in path": See https://github.com/ocaml/num/issues/9
+ 59: "potential assignment to a non-mutable value": See Coq's issue #8043
*)
-let coq_warnings = "-w +a-4-9-27-41-42-44-45-48-50"
+let coq_warnings = "-w +a-4-9-27-41-42-44-45-48-50-58-59"
let coq_warn_error =
if !prefs.warn_error
then "-warn-error +a"
@@ -1337,6 +1339,7 @@ let write_makefile f =
pr "WITHDOC=%s\n\n" (if !prefs.withdoc then "all" else "no");
pr "# Option to produce precompiled files for native_compute\n";
pr "NATIVECOMPUTE=%s\n" (if !prefs.nativecompiler then "-native-compiler" else "");
+ pr "COQWARNERROR=%s\n" (if !prefs.warn_error then "-w +default" else "");
close_out o;
Unix.chmod f 0o444
diff --git a/dev/tools/check-overlays.sh b/dev/tools/check-overlays.sh
index f7e05b51c..33a9ff058 100755
--- a/dev/tools/check-overlays.sh
+++ b/dev/tools/check-overlays.sh
@@ -1,8 +1,8 @@
#!/usr/bin/env bash
-for f in dev/ci/user-overlays/*
+for f in $(git ls-files "dev/ci/user-overlays/")
do
- if ! ([[ $f = dev/ci/user-overlays/README.md ]] || [[ $f == *.sh ]])
+ if ! ([[ "$f" = dev/ci/user-overlays/README.md ]] || [[ "$f" == *.sh ]])
then
>&2 echo "Bad overlay '$f'."
>&2 echo "User overlays need to have extension .sh to be picked up!"
diff --git a/doc/sphinx/credits.rst b/doc/sphinx/credits.rst
index 5d9324a65..2988b194e 100644
--- a/doc/sphinx/credits.rst
+++ b/doc/sphinx/credits.rst
@@ -40,7 +40,7 @@ foundation of mathematics on constructive principles. The second one,
Girard’s polymorphic :math:`\lambda`-calculus :math:`F_\omega`, is a
very strong functional system in which we may represent higher-order
logic proof structures. Combining both systems in a higher-order
-extension of the Automath languages, T. Coquand presented in 1985 the
+extension of the Automath language, T. Coquand presented in 1985 the
first version of the *Calculus of Constructions*, CoC. This strong
logical system allowed powerful axiomatizations, but direct inductive
definitions were not possible, and inductive notions had to be defined
@@ -246,14 +246,14 @@ pretty-printing rules has also changed.
Eduardo Giménez redesigned the internal tactic libraries, giving uniform
names to Caml functions corresponding to |Coq| tactic names.
-Bruno Barras wrote new more efficient reductions functions.
+Bruno Barras wrote new, more efficient reduction functions.
Hugo Herbelin introduced more uniform notations in the |Coq| specification
language: the definitions by fixpoints and pattern-matching have a more
readable syntax. Patrick Loiseleur introduced user-friendly notations
for arithmetic expressions.
-New tactics were introduced: Eduardo Giménez improved a mechanism to
+New tactics were introduced: Eduardo Giménez improved the mechanism to
introduce macros for tactics, and designed special tactics for
(co)inductive definitions; Patrick Loiseleur designed a tactic to
simplify polynomial expressions in an arbitrary commutative ring which
@@ -279,12 +279,12 @@ Loiseleur.
Credits: addendum for version 6.3
=================================
-The main changes in version V6.3 was the introduction of a few new
+The main changes in version V6.3 were the introduction of a few new
tactics and the extension of the guard condition for fixpoint
definitions.
B. Barras extended the unification algorithm to complete partial terms
-and solved various tricky bugs related to universes.
+and fixed various tricky bugs related to universes.
D. Delahaye developed the ``AutoRewrite`` tactic. He also designed the
new behavior of ``Intro`` and provided the tacticals ``First`` and
@@ -318,8 +318,8 @@ internal architecture of the system. The |Coq| version 7.0 was distributed
in March 2001, version 7.1 in September 2001, version 7.2 in January
2002, version 7.3 in May 2002 and version 7.4 in February 2003.
-Jean-Christophe Filliâtre designed the architecture of the new system,
-he introduced a new representation for environments and wrote a new
+Jean-Christophe Filliâtre designed the architecture of the new system.
+He introduced a new representation for environments and wrote a new
kernel for type-checking terms. His approach was to use functional
data-structures in order to get more sharing, to prepare the addition of
modules and also to get closer to a certified kernel.
@@ -351,7 +351,7 @@ Letouzey adapted user contributions to extract ML programs when it was
sensible. Jean-Christophe Filliâtre wrote ``coqdoc``, a documentation
tool for |Coq| libraries usable from version 7.2.
-Bruno Barras improved the reduction algorithms efficiency and the
+Bruno Barras improved the efficiency of the reduction algorithm and the
confidence level in the correctness of |Coq| critical type-checking
algorithm.
@@ -368,8 +368,8 @@ propositional inductive types.
Loïc Pottier developed Fourier, a tactic solving linear inequalities on
real numbers.
-Pierre Crégut developed a new version based on reflexion of the Omega
-decision tactic.
+Pierre Crégut developed a new, reflection-based version of the Omega
+decision procedure.
Claudio Sacerdoti Coen designed an XML output for the |Coq| modules to be
used in the Hypertextual Electronic Library of Mathematics (HELM cf
@@ -419,7 +419,7 @@ main motivations were
with a functional programming perfume (e.g. abstraction is now
written fun), and more directly accessible to the novice (e.g.
dependent product is now written forall and allows omission of
- types). Also, parentheses and are no longer mandatory for function
+ types). Also, parentheses are no longer mandatory for function
application.
- extensibility: some standard notations (e.g. “<” and “>”) were
@@ -438,8 +438,8 @@ language and of the language of commands has been carried out. The
purpose here is a better uniformity making the tactics and commands
easier to use and to remember.
-Thirdly, a restructuration and uniformisation of the standard library of
-Coq has been performed. There is now just one Leibniz’ equality usable
+Thirdly, a restructuring and uniformization of the standard library of
+Coq has been performed. There is now just one Leibniz equality usable
for all the different kinds of |Coq| objects. Also, the set of real
numbers now lies at the same level as the sets of natural and integer
numbers. Finally, the names of the standard properties of numbers now
@@ -447,7 +447,7 @@ follow a standard pattern and the symbolic notations for the standard
definitions as well.
The fourth point is the release of |CoqIDE|, a new graphical gtk2-based
-interface fully integrated to |Coq|. Close in style from the Proof General
+interface fully integrated with |Coq|. Close in style to the Proof General
Emacs interface, it is faster and its integration with |Coq| makes
interactive developments more friendly. All mathematical Unicode symbols
are usable within |CoqIDE|.
@@ -461,18 +461,17 @@ improved tactics (including a new tactic for solving first-order
statements), new management commands, extended libraries.
Bruno Barras and Hugo Herbelin have been the main contributors of the
-reflexion and the implementation of the new syntax. The smart automatic
+reflection and the implementation of the new syntax. The smart automatic
translator from old to new syntax released with |Coq| is also their work
with contributions by Olivier Desmettre.
-Hugo Herbelin is the main designer and implementor of the notion of
+Hugo Herbelin is the main designer and implementer of the notion of
interpretation scopes and of the commands for easily adding new
notations.
-Hugo Herbelin is the main implementor of the restructuration of the
-standard library.
+Hugo Herbelin is the main implementer of the restructured standard library.
-Pierre Corbineau is the main designer and implementor of the new tactic
+Pierre Corbineau is the main designer and implementer of the new tactic
for solving first-order statements in presence of inductive types. He is
also the maintainer of the non-domain specific automation tactics.
@@ -487,14 +486,14 @@ Pierre Letouzey and Jacek Chrząszcz respectively maintained the
extraction tool and module system of |Coq|.
Jean-Christophe Filliâtre, Pierre Letouzey, Hugo Herbelin and other
-contributors from Sophia-Antipolis and Nijmegen participated to the
-extension of the library.
+contributors from Sophia-Antipolis and Nijmegen participated in
+extending the library.
Julien Narboux built a NSIS-based automatic |Coq| installation tool for
the Windows platform.
Hugo Herbelin and Christine Paulin coordinated the development which was
-under the responsability of Christine Paulin.
+under the responsibility of Christine Paulin.
| Palaiseau & Orsay, Apr. 2004
| Hugo Herbelin & Christine Paulin
@@ -525,12 +524,12 @@ arbitrary transition systems.
Claudio Sacerdoti Coen added new features to the module system.
-Benjamin Grégoire, Assia Mahboubi and Bruno Barras developed a new more
-efficient and more general simplification algorithm on rings and
+Benjamin Grégoire, Assia Mahboubi and Bruno Barras developed a new, more
+efficient and more general simplification algorithm for rings and
semi-rings.
-Laurent Théry and Bruno Barras developed a new significantly more
-efficient simplification algorithm on fields.
+Laurent Théry and Bruno Barras developed a new, significantly more
+efficient simplification algorithm for fields.
Hugo Herbelin, Pierre Letouzey, Julien Forest, Julien Narboux and
Claudio Sacerdoti Coen added new tactic features.
@@ -554,7 +553,7 @@ Jean-Christophe Filliâtre’s contribution on finite maps have been
integrated to the |Coq| standard library. Pierre Letouzey developed a
library about finite sets “à la Objective Caml”. With Jean-Marc Notin,
he extended the library on lists. Pierre Letouzey’s contribution on
-rational numbers has been integrated and extended..
+rational numbers has been integrated and extended.
Pierre Corbineau extended his tactic for solving first-order statements.
He wrote a reflection-based intuitionistic tautology solver.
@@ -589,8 +588,8 @@ various aspects.
Regarding the language of |Coq|, the main novelty is the introduction by
Matthieu Sozeau of a package of commands providing Haskell-style type
classes. Type classes, that come with a few convenient features such as
-type-based resolution of implicit arguments, plays a new role of
-landmark in the architecture of |Coq| with respect to automatization. For
+type-based resolution of implicit arguments, play a new landmark role
+in the architecture of |Coq| with respect to automation. For
instance, thanks to type classes support, Matthieu Sozeau could
implement a new resolution-based version of the tactics dedicated to
rewriting on arbitrary transitive relations.
@@ -599,13 +598,13 @@ Another major improvement of |Coq| 8.2 is the evolution of the arithmetic
libraries and of the tools associated to them. Benjamin Grégoire and
Laurent Théry contributed a modular library for building arbitrarily
large integers from bounded integers while Evgeny Makarov contributed a
-modular library of abstract natural and integer arithmetics together
+modular library of abstract natural and integer arithmetic together
with a few convenient tactics. On his side, Pierre Letouzey made
numerous extensions to the arithmetic libraries on :math:`\mathbb{Z}`
-and :math:`\mathbb{Q}`, including extra support for automatization in
+and :math:`\mathbb{Q}`, including extra support for automation in
presence of various number-theory concepts.
-Frédéric Besson contributed a reflexive tactic based on Krivine-Stengle
+Frédéric Besson contributed a reflective tactic based on Krivine-Stengle
Positivstellensatz (the easy way) for validating provability of systems
of inequalities. The platform is flexible enough to support the
validation of any algorithm able to produce a “certificate” for the
@@ -620,10 +619,10 @@ relying on Benjamin Grégoire and Laurent Théry’s library, delivered a
library of unbounded integers in base :math:`2^{31}`. As importantly, he
developed a notion of “retro-knowledge” so as to safely extend the
kernel-located bytecode-based efficient evaluation algorithm of |Coq|
-version 8.1 to use 31-bits machine arithmetics for efficiently computing
+version 8.1 to use 31-bits machine arithmetic for efficiently computing
with the library of integers he developed.
-Beside the libraries, various improvements contributed to provide a more
+Beside the libraries, various improvements were contributed to provide a more
comfortable end-user language and more expressive tactic language. Hugo
Herbelin and Matthieu Sozeau improved the pattern-matching compilation
algorithm (detection of impossible clauses in pattern-matching,
@@ -632,7 +631,7 @@ and Matthieu Sozeau contributed various new convenient syntactic
constructs and new tactics or tactic features: more inference of
redundant information, better unification, better support for proof or
definition by fixpoint, more expressive rewriting tactics, better
-support for meta-variables, more convenient notations, ...
+support for meta-variables, more convenient notations...
Élie Soubiran improved the module system, adding new features (such as
an “include” command) and making it more flexible and more general. He
@@ -641,7 +640,7 @@ mechanism.
Matthieu Sozeau extended the Russell language, ending in an convenient
way to write programs of given specifications, Pierre Corbineau extended
-the Mathematical Proof Language and the automatization tools that
+the Mathematical Proof Language and the automation tools that
accompany it, Pierre Letouzey supervised and extended various parts of the
standard library, Stéphane Glondu contributed a few tactics and
improvements, Jean-Marc Notin provided help in debugging, general
@@ -662,7 +661,7 @@ adaptation of the interface of the old “setoid rewrite” tactic to the
new version. Lionel Mamane worked on the interaction between |Coq| and its
external interfaces. With Samuel Mimram, he also helped making |Coq|
compatible with recent software tools. Russell O’Connor, Cezary
-Kaliscyk, Milad Niqui contributed to improve the libraries of integers,
+Kaliszyk, Milad Niqui contributed to improve the libraries of integers,
rational, and real numbers. We also thank many users and partners for
suggestions and feedback, in particular Pierre Castéran and Arthur
Charguéraud, the INRIA Marelle team, Georges Gonthier and the
@@ -704,8 +703,8 @@ The module system evolved significantly. Besides the resolution of some
efficiency issues and a more flexible construction of module types, Élie
Soubiran brought a new model of name equivalence, the
:math:`\Delta`-equivalence, which respects as much as possible the names
-given by the users. He also designed with Pierre Letouzey a new
-convenient operator ``<+`` for nesting functor application, that
+given by the users. He also designed with Pierre Letouzey a new,
+convenient operator ``<+`` for nesting functor application that
provides a light notation for inheriting the properties of cascading
modules.
@@ -719,7 +718,7 @@ the extraction mechanism. Bruno Barras and Élie Soubiran maintained the
Coq checker, Julien Forest maintained the Function mechanism for
reasoning over recursively defined functions. Matthieu Sozeau, Hugo
Herbelin and Jean-Marc Notin maintained coqdoc. Frédéric Besson
-maintained the Micromega plateform for deciding systems of inequalities.
+maintained the Micromega platform for deciding systems of inequalities.
Pierre Courtieu maintained the support for the Proof General Emacs
interface. Claude Marché maintained the plugin for calling external
provers (dp). Yves Bertot made some improvements to the libraries of
@@ -736,7 +735,7 @@ support for benchmarking and archiving.
Many users helped by reporting problems, providing patches, suggesting
improvements or making useful comments, either on the bug tracker or on
-the Coq-club mailing list. This includes but not exhaustively Cédric
+the Coq-Club mailing list. This includes but not exhaustively Cédric
Auger, Arthur Charguéraud, François Garillot, Georges Gonthier, Robin
Green, Stéphane Lescuyer, Eelis van der Weegen, ...
@@ -772,8 +771,8 @@ structured scripts (bullets and proof brackets) but, even if yet not
user-available, the new engine also provides the basis for refining
existential variables using tactics, for applying tactics to several
goals simultaneously, for reordering goals, all features which are
-planned for the next release. The new proof engine forced to reimplement
-info and Show Script differently, what was done by Pierre Letouzey.
+planned for the next release. The new proof engine forced Pierre Letouzey
+to reimplement info and Show Script differently.
Before version 8.4, |CoqIDE| was linked to |Coq| with the graphical
interface living in a separate thread. From version 8.4, |CoqIDE| is a
@@ -784,7 +783,7 @@ sessions in parallel. Relying on the infrastructure work made by Vincent
Gross, Pierre Letouzey, Pierre Boutillier and Pierre-Marie Pédrot
contributed many various refinements of |CoqIDE|.
-Coq 8.4 also comes with a bunch of many various smaller-scale changes
+Coq 8.4 also comes with a bunch of various smaller-scale changes
and improvements regarding the different components of the system.
The underlying logic has been extended with :math:`\eta`-conversion
@@ -831,7 +830,7 @@ Pierre Letouzey added a tactic timeout and the interruptibility of
vm\_compute. Bug fixes and miscellaneous improvements of the tactic
language came from Hugo Herbelin, Pierre Letouzey and Matthieu Sozeau.
-Regarding decision tactics, Loïc Pottier maintained Nsatz, moving in
+Regarding decision tactics, Loïc Pottier maintained nsatz, moving in
particular to a type-class based reification of goals while Frédéric
Besson maintained Micromega, adding in particular support for division.
@@ -894,7 +893,7 @@ Boutillier (MacOS), Stéphane Glondu (Debian). Releasing, testing and
benchmarking support was provided by Jean-Marc Notin.
Many suggestions for improvements were motivated by feedback from users,
-on either the bug tracker or the coq-club mailing list. Special thanks
+on either the bug tracker or the Coq-Club mailing list. Special thanks
are going to the users who contributed patches, starting with Tom
Prince. Other patch contributors include Cédric Auger, David Baelde, Dan
Grayson, Paolo Herms, Robbert Krebbers, Marc Lasson, Hendrik Tews and
@@ -1036,7 +1035,7 @@ X). Maxime Dénès improved significantly the testing and benchmarking
support.
Many power users helped to improve the design of the new features via
-the bug tracker, the coq development mailing list or the coq-club
+the bug tracker, the coq development mailing list or the Coq-Club
mailing list. Special thanks are going to the users who contributed
patches and intensive brain-storming, starting with Jason Gross,
Jonathan Leivent, Greg Malecha, Clément Pit-Claudel, Marc Lasson, Lionel
@@ -1154,13 +1153,13 @@ Gregory Malecha, and Matthieu Sozeau.
Matej Košík maintained and greatly improved the continuous integration
setup and the testing of |Coq| contributions. He also contributed many API
-improvement and code cleanups throughout the system.
+improvements and code cleanups throughout the system.
The contributors for this version are Bruno Barras, C.J. Bell, Yves
Bertot, Frédéric Besson, Pierre Boutillier, Tej Chajed, Guillaume
Claret, Xavier Clerc, Pierre Corbineau, Pierre Courtieu, Maxime Dénès,
Ricky Elrod, Emilio Jesús Gallego Arias, Jason Gross, Hugo Herbelin,
-Sébastien Hinderer, Jacques-Henri Jourdan, Matej Kosik, Xavier Leroy,
+Sébastien Hinderer, Jacques-Henri Jourdan, Matej Košík, Xavier Leroy,
Pierre Letouzey, Gregory Malecha, Cyprien Mangin, Erik Martin-Dorel,
Guillaume Melquiond, Clément Pit–Claudel, Pierre-Marie Pédrot, Daniel de
Rauglaudre, Lionel Rieg, Gabriel Scherer, Thomas Sibut-Pinote, Matthieu
@@ -1171,7 +1170,7 @@ Dénès, who was also in charge of the release process.
Many power users helped to improve the design of the new features via
the bug tracker, the pull request system, the |Coq| development mailing
-list or the coq-club mailing list. Special thanks to the users who
+list or the Coq-Club mailing list. Special thanks to the users who
contributed patches and intensive brain-storming and code reviews,
starting with Cyril Cohen, Jason Gross, Robbert Krebbers, Jonathan
Leivent, Xavier Leroy, Gregory Malecha, Clément Pit–Claudel, Gabriel
@@ -1279,7 +1278,7 @@ the maintainer of this release.
Many power users helped to improve the design of the new features via the bug
tracker, the pull request system, the |Coq| development mailing list or the
-coq-club mailing list. Special thanks to the users who contributed patches and
+Coq-Club mailing list. Special thanks to the users who contributed patches and
intensive brain-storming and code reviews, starting with Jason Gross, Ralf Jung,
Robbert Krebbers, Xavier Leroy, Clément Pit–Claudel and Gabriel Scherer. It
would however be impossible to mention exhaustively the names of everybody who
diff --git a/doc/sphinx/introduction.rst b/doc/sphinx/introduction.rst
index c7bc69db4..1a610396e 100644
--- a/doc/sphinx/introduction.rst
+++ b/doc/sphinx/introduction.rst
@@ -12,7 +12,7 @@ https://github.com/coq/coq/wiki#coq-tutorials).
The |Coq| system is designed to develop mathematical proofs, and
especially to write formal specifications, programs and to verify that
-programs are correct with respect to their specification. It provides a
+programs are correct with respect to their specifications. It provides a
specification language named |Gallina|. Terms of |Gallina| can represent
programs as well as properties of these programs and proofs of these
properties. Using the so-called *Curry-Howard isomorphism*, programs,
@@ -52,7 +52,7 @@ are processed from a file.
How to read this book
=====================
-This is a Reference Manual, so it is not made for a continuous reading.
+This is a Reference Manual, so it is not intended for continuous reading.
We recommend using the various indexes to quickly locate the documentation
you are looking for. There is a global index, and a number of specific indexes
for tactics, vernacular commands, and error messages and warnings.
diff --git a/kernel/retroknowledge.ml b/kernel/retroknowledge.ml
index d76b05a8b..34f62defb 100644
--- a/kernel/retroknowledge.ml
+++ b/kernel/retroknowledge.ml
@@ -25,22 +25,6 @@ open Constr
(* aliased type for clarity purpose*)
type entry = Constr.t
-(* [field]-s are the roles the kernel can learn of. *)
-type nat_field =
- | NatType
- | NatPlus
- | NatTimes
-
-type n_field =
- | NPositive
- | NType
- | NTwice
- | NTwicePlusOne
- | NPhi
- | NPhiInv
- | NPlus
- | NTimes
-
type int31_field =
| Int31Bits
| Int31Type
@@ -69,9 +53,6 @@ type int31_field =
| Int31Lxor
type field =
- (* | KEq
- | KNat of nat_field
- | KN of n_field *)
| KInt31 of string*int31_field
diff --git a/kernel/retroknowledge.mli b/kernel/retroknowledge.mli
index 281c37b85..02d961d89 100644
--- a/kernel/retroknowledge.mli
+++ b/kernel/retroknowledge.mli
@@ -18,21 +18,6 @@ type entry = Constr.t
(** the following types correspond to the different "things"
the kernel can learn about.*)
-type nat_field =
- | NatType
- | NatPlus
- | NatTimes
-
-type n_field =
- | NPositive
- | NType
- | NTwice
- | NTwicePlusOne
- | NPhi
- | NPhiInv
- | NPlus
- | NTimes
-
type int31_field =
| Int31Bits
| Int31Type
@@ -61,13 +46,8 @@ type int31_field =
| Int31Lxor
type field =
-
-(** | KEq
- | KNat of nat_field
- | KN of n_field *)
| KInt31 of string*int31_field
-
(** This type represent an atomic action of the retroknowledge. It
is stored in the compiled libraries
As per now, there is only the possibility of registering things
diff --git a/plugins/ltac/extraargs.ml4 b/plugins/ltac/extraargs.ml4
index dae2582bd..dbbdbfa39 100644
--- a/plugins/ltac/extraargs.ml4
+++ b/plugins/ltac/extraargs.ml4
@@ -297,25 +297,6 @@ END
(* spiwack: the print functions are incomplete, but I don't know what they are
used for *)
-let pr_r_nat_field natf =
- str "nat " ++
- match natf with
- | Retroknowledge.NatType -> str "type"
- | Retroknowledge.NatPlus -> str "plus"
- | Retroknowledge.NatTimes -> str "times"
-
-let pr_r_n_field nf =
- str "binary N " ++
- match nf with
- | Retroknowledge.NPositive -> str "positive"
- | Retroknowledge.NType -> str "type"
- | Retroknowledge.NTwice -> str "twice"
- | Retroknowledge.NTwicePlusOne -> str "twice plus one"
- | Retroknowledge.NPhi -> str "phi"
- | Retroknowledge.NPhiInv -> str "phi inv"
- | Retroknowledge.NPlus -> str "plus"
- | Retroknowledge.NTimes -> str "times"
-
let pr_r_int31_field i31f =
str "int31 " ++
match i31f with
@@ -353,26 +334,6 @@ let pr_retroknowledge_field f =
| Retroknowledge.KInt31 (group, i31f) -> (pr_r_int31_field i31f) ++
spc () ++ str "in " ++ qs group
-VERNAC ARGUMENT EXTEND retroknowledge_nat
-PRINTED BY pr_r_nat_field
-| [ "nat" "type" ] -> [ Retroknowledge.NatType ]
-| [ "nat" "plus" ] -> [ Retroknowledge.NatPlus ]
-| [ "nat" "times" ] -> [ Retroknowledge.NatTimes ]
-END
-
-
-VERNAC ARGUMENT EXTEND retroknowledge_binary_n
-PRINTED BY pr_r_n_field
-| [ "binary" "N" "positive" ] -> [ Retroknowledge.NPositive ]
-| [ "binary" "N" "type" ] -> [ Retroknowledge.NType ]
-| [ "binary" "N" "twice" ] -> [ Retroknowledge.NTwice ]
-| [ "binary" "N" "twice" "plus" "one" ] -> [ Retroknowledge.NTwicePlusOne ]
-| [ "binary" "N" "phi" ] -> [ Retroknowledge.NPhi ]
-| [ "binary" "N" "phi" "inv" ] -> [ Retroknowledge.NPhiInv ]
-| [ "binary" "N" "plus" ] -> [ Retroknowledge.NPlus ]
-| [ "binary" "N" "times" ] -> [ Retroknowledge.NTimes ]
-END
-
VERNAC ARGUMENT EXTEND retroknowledge_int31
PRINTED BY pr_r_int31_field
| [ "int31" "bits" ] -> [ Retroknowledge.Int31Bits ]
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-27 21:56:27 +0000