aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--.gitignore1
-rw-r--r--.gitlab-ci.yml1
-rw-r--r--Makefile.doc2
-rw-r--r--checker/indtypes.ml46
-rw-r--r--checker/inductive.ml33
-rw-r--r--checker/subtyping.ml8
-rwxr-xr-xdev/ci/ci-sf.sh9
-rwxr-xr-xdoc/sphinx/conf.py5
-rw-r--r--doc/sphinx/credits.html.rst7
-rw-r--r--doc/sphinx/credits.latex.rst3
-rw-r--r--doc/sphinx/credits.rst (renamed from doc/sphinx/credits-contents.rst)32
-rw-r--r--doc/sphinx/index.html.rst11
-rw-r--r--doc/sphinx/index.latex.rst16
-rw-r--r--doc/sphinx/introduction.rst4
-rw-r--r--doc/sphinx/license.rst3
-rw-r--r--doc/sphinx/practical-tools/utilities.rst13
-rw-r--r--doc/sphinx/proof-engine/proof-handling.rst13
-rw-r--r--doc/sphinx/proof-engine/tactics.rst2
-rw-r--r--doc/sphinx/proof-engine/vernacular-commands.rst1
19 files changed, 118 insertions, 92 deletions
diff --git a/.gitignore b/.gitignore
index 39ef20970d..05869e2a0c 100644
--- a/.gitignore
+++ b/.gitignore
@@ -101,7 +101,6 @@ doc/faq/axioms.pdf_t
doc/faq/axioms.png
doc/sphinx/index.rst
doc/sphinx/zebibliography.rst
-doc/sphinx/credits.rst
doc/stdlib/Library.out
doc/stdlib/Library.ps
doc/stdlib/Library.coqdoc.tex
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index e829b517d7..1669145d9b 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -366,6 +366,7 @@ ci-aac-tactics:
ci-bedrock2:
<<: *ci-template
+ allow_failure: true
ci-bignums:
<<: *ci-template
diff --git a/Makefile.doc b/Makefile.doc
index 1184cc186b..9e6ec4955a 100644
--- a/Makefile.doc
+++ b/Makefile.doc
@@ -10,7 +10,7 @@
# Makefile for the Coq documentation
-# Read INSTALL.doc to learn about the dependencies
+# Read doc/README.md to learn about the dependencies
# The main entry point :
diff --git a/checker/indtypes.ml b/checker/indtypes.ml
index 0478765a81..50e65ef587 100644
--- a/checker/indtypes.ml
+++ b/checker/indtypes.ml
@@ -310,25 +310,31 @@ let failwith_non_pos_list n ntypes l =
List.iter (failwith_non_pos n ntypes) l;
anomaly ~label:"failwith_non_pos_list" (Pp.str "some k in [n;n+ntypes-1] should occur.")
-(* Conclusion of constructors: check the inductive type is called with
- the expected parameters *)
-let check_correct_par (env,n,ntypes,_) hyps l largs =
- let nparams = rel_context_nhyps hyps in
- let largs = Array.of_list largs in
- if Array.length largs < nparams then
- raise (IllFormedInd (LocalNotEnoughArgs l));
- let (lpar,largs') = Array.chop nparams largs in
- let nhyps = List.length hyps in
- let rec check k index = function
+(* Check the inductive type is called with the expected parameters *)
+(* [n] is the index of the last inductive type in [env] *)
+let check_correct_par (env,n,ntypes,_) paramdecls ind_index args =
+ let nparams = rel_context_nhyps paramdecls in
+ let args = Array.of_list args in
+ if Array.length args < nparams then
+ raise (IllFormedInd (LocalNotEnoughArgs ind_index));
+ let (params,realargs) = Array.chop nparams args in
+ let nparamdecls = List.length paramdecls in
+ let rec check param_index paramdecl_index = function
| [] -> ()
- | LocalDef _ :: hyps -> check k (index+1) hyps
- | _::hyps ->
- match whd_all env lpar.(k) with
- | Rel w when w = index -> check (k-1) (index+1) hyps
- | _ -> raise (IllFormedInd (LocalNonPar (k+1,index,l)))
- in check (nparams-1) (n-nhyps) hyps;
- if not (Array.for_all (noccur_between n ntypes) largs') then
- failwith_non_pos_vect n ntypes largs'
+ | LocalDef _ :: paramdecls ->
+ check param_index (paramdecl_index+1) paramdecls
+ | _::paramdecls ->
+ match whd_all env params.(param_index) with
+ | Rel w when Int.equal w paramdecl_index ->
+ check (param_index-1) (paramdecl_index+1) paramdecls
+ | _ ->
+ let paramdecl_index_in_env = paramdecl_index-n+nparamdecls+1 in
+ let err =
+ LocalNonPar (param_index+1, paramdecl_index_in_env, ind_index) in
+ raise (IllFormedInd err)
+ in check (nparams-1) (n-nparamdecls) paramdecls;
+ if not (Array.for_all (noccur_between n ntypes) realargs) then
+ failwith_non_pos_vect n ntypes realargs
(* Arguments of constructor: check the number of recursive parameters nrecp.
the first parameters which are constant in recursive arguments
@@ -412,8 +418,8 @@ let check_positivity_one (env, _,ntypes,_ as ienv) hyps nrecp (_,i as ind) indlc
| Some b ->
check_pos (ienv_push_var ienv (na, b, mk_norec)) d)
| Rel k ->
- (try
- let (ra,rarg) = List.nth ra_env (k-1) in
+ (try let (ra,rarg) = List.nth ra_env (k-1) in
+ let largs = List.map (whd_all env) largs in
(match ra with
Mrec _ -> check_rec_par ienv hyps nrecp largs
| _ -> ());
diff --git a/checker/inductive.ml b/checker/inductive.ml
index d15380643f..5e34f04f51 100644
--- a/checker/inductive.ml
+++ b/checker/inductive.ml
@@ -282,6 +282,11 @@ let get_instantiated_arity (ind,u) (mib,mip) params =
let elim_sorts (_,mip) = mip.mind_kelim
+let is_primitive_record (mib,_) =
+ match mib.mind_record with
+ | PrimRecord _ -> true
+ | NotRecord | FakeRecord -> false
+
let extended_rel_list n hyps =
let rec reln l p = function
| LocalAssum _ :: hyps -> reln (Rel (n+p) :: l) (p+1) hyps
@@ -381,12 +386,13 @@ let type_case_branches env (pind,largs) (p,pj) c =
(* Checking the case annotation is relevant *)
let check_case_info env indsp ci =
- let (mib,mip) = lookup_mind_specif env indsp in
+ let mib, mip as spec = lookup_mind_specif env indsp in
if
not (eq_ind_chk indsp ci.ci_ind) ||
(mib.mind_nparams <> ci.ci_npar) ||
(mip.mind_consnrealdecls <> ci.ci_cstr_ndecls) ||
- (mip.mind_consnrealargs <> ci.ci_cstr_nargs)
+ (mip.mind_consnrealargs <> ci.ci_cstr_nargs) ||
+ is_primitive_record spec
then raise (TypeError(env,WrongCaseInfo(indsp,ci)))
(************************************************************************)
@@ -801,10 +807,23 @@ let rec subterm_specif renv stack t =
subterm_specif (push_var renv (x,a,spec)) stack' b
(* Metas and evars are considered OK *)
- | (Meta _|Evar _) -> Dead_code
-
- (* Other terms are not subterms *)
- | _ -> Not_subterm
+ | (Meta _|Evar _) -> Dead_code
+
+ | Proj (p, c) ->
+ let subt = subterm_specif renv stack c in
+ (match subt with
+ | Subterm (_s, wf) ->
+ (* We take the subterm specs of the constructor of the record *)
+ let wf_args = (dest_subterms wf).(0) in
+ (* We extract the tree of the projected argument *)
+ let n = Projection.arg p in
+ spec_of_tree (List.nth wf_args n)
+ | Dead_code -> Dead_code
+ | Not_subterm -> Not_subterm)
+
+ (* Other terms are not subterms *)
+ | Var _ | Sort _ | Cast _ | Prod _ | LetIn _ | App _ | Const _ | Ind _
+ | Construct _ | CoFix _ -> Not_subterm
and lazy_subterm_specif renv stack t =
lazy (subterm_specif renv stack t)
@@ -856,6 +875,8 @@ let filter_stack_domain env p stack =
match stack, t with
| elt :: stack', Prod (n,a,c0) ->
let d = LocalAssum (n,a) in
+ let ctx, a = dest_prod_assum env a in
+ let env = push_rel_context ctx env in
let ty, args = decompose_app (whd_all env a) in
let elt = match ty with
| Ind ind ->
diff --git a/checker/subtyping.ml b/checker/subtyping.ml
index 0916d98ddf..e2c605dde8 100644
--- a/checker/subtyping.ml
+++ b/checker/subtyping.ml
@@ -198,9 +198,11 @@ let check_inductive env mp1 l info1 mib2 spec2 subst1 subst2=
assert (Array.length mib2.mind_packets = 1);
assert (Array.length mib1.mind_packets.(0).mind_user_lc = 1);
assert (Array.length mib2.mind_packets.(0).mind_user_lc = 1);
- check
- (fun l1 l2 -> List.equal Name.equal l1 l2)
- (fun mib -> names_prod_letin mib.mind_packets.(0).mind_user_lc.(0));
+ check (List.equal Name.equal)
+ (fun mib ->
+ let nparamdecls = List.length mib.mind_params_ctxt in
+ let names = names_prod_letin (mib.mind_packets.(0).mind_user_lc.(0)) in
+ snd (List.chop nparamdecls names))
end;
(* we first check simple things *)
Array.iter2 check_packet mib1.mind_packets mib2.mind_packets;
diff --git a/dev/ci/ci-sf.sh b/dev/ci/ci-sf.sh
index 58bbb7229f..60436e672c 100755
--- a/dev/ci/ci-sf.sh
+++ b/dev/ci/ci-sf.sh
@@ -8,11 +8,6 @@ wget -qO- "${sf_lf_CI_TARURL}" | tar xvz
wget -qO- "${sf_plf_CI_TARURL}" | tar xvz
wget -qO- "${sf_vfa_CI_TARURL}" | tar xvz
-sed -i.bak '1i From Coq Require Extraction.' lf/Extraction.v
-sed -i.bak '1i From Coq Require Extraction.' vfa/Extract.v
-
-( cd lf && make clean && make )
-
-( cd plf && sed -i.bak 's/(K,N)/((K,N))/' LibTactics.v && make clean && make )
-
+( cd lf && make clean && make )
+( cd plf && make clean && make )
( cd vfa && make clean && make )
diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py
index 71f01cbb17..d98b8641e9 100755
--- a/doc/sphinx/conf.py
+++ b/doc/sphinx/conf.py
@@ -193,8 +193,9 @@ html_theme = 'sphinx_rtd_theme'
# Theme options are theme-specific and customize the look and feel of a theme
# further. For a list of options available for each theme, see the
# documentation.
-#html_theme_options = {}
-
+html_theme_options = {
+ 'collapse_navigation': False
+}
html_context = {
'display_github': True,
'github_user': 'coq',
diff --git a/doc/sphinx/credits.html.rst b/doc/sphinx/credits.html.rst
deleted file mode 100644
index 0b2b1c6ad1..0000000000
--- a/doc/sphinx/credits.html.rst
+++ /dev/null
@@ -1,7 +0,0 @@
-.. _credits:
-
--------
-Credits
--------
-
-.. include:: credits-contents.rst
diff --git a/doc/sphinx/credits.latex.rst b/doc/sphinx/credits.latex.rst
deleted file mode 100644
index 39101f9d52..0000000000
--- a/doc/sphinx/credits.latex.rst
+++ /dev/null
@@ -1,3 +0,0 @@
-.. _credits:
-
-.. include:: credits-contents.rst
diff --git a/doc/sphinx/credits-contents.rst b/doc/sphinx/credits.rst
index d1df0657aa..ffdc4f3ec6 100644
--- a/doc/sphinx/credits-contents.rst
+++ b/doc/sphinx/credits.rst
@@ -1,3 +1,7 @@
+-------
+Credits
+-------
+
Coq is a proof assistant for higher-order logic, allowing the
development of computer programs consistent with their formal
specification. It is the result of about ten years of research of the
@@ -186,7 +190,7 @@ definitions of “inversion predicates”.
|
Credits: addendum for version 6.1
-=================================
+---------------------------------
The present version 6.1 of |Coq| is based on the V5.10 architecture. It
was ported to the new language Objective Caml by Bruno Barras. The
@@ -223,7 +227,7 @@ Barras.
|
Credits: addendum for version 6.2
-=================================
+---------------------------------
In version 6.2 of |Coq|, the parsing is done using camlp4, a preprocessor
and pretty-printer for CAML designed by Daniel de Rauglaudre at INRIA.
@@ -268,7 +272,7 @@ Loiseleur.
|
Credits: addendum for version 6.3
-=================================
+---------------------------------
The main changes in version V6.3 were the introduction of a few new
tactics and the extension of the guard condition for fixpoint
@@ -301,7 +305,7 @@ Monin from CNET Lannion.
|
Credits: versions 7
-===================
+-------------------
The version V7 is a new implementation started in September 1999 by
Jean-Christophe Filliâtre. This is a major revision with respect to the
@@ -390,7 +394,7 @@ J.-F. Monin from France Telecom R & D.
|
Credits: version 8.0
-====================
+--------------------
Coq version 8 is a major revision of the |Coq| proof assistant. First, the
underlying logic is slightly different. The so-called *impredicativity*
@@ -492,7 +496,7 @@ under the responsibility of Christine Paulin.
|
Credits: version 8.1
-====================
+--------------------
Coq version 8.1 adds various new functionalities.
@@ -571,7 +575,7 @@ and Yale University.
|
Credits: version 8.2
-====================
+--------------------
Coq version 8.2 adds new features, new libraries and improves on many
various aspects.
@@ -665,7 +669,7 @@ the Coq-Club mailing list.
|
Credits: version 8.3
-====================
+--------------------
Coq version 8.3 is before all a transition version with refinements or
extensions of the existing features and libraries and a new tactic nsatz
@@ -739,7 +743,7 @@ Pierce for the excellent teaching materials they provided.
|
Credits: version 8.4
-====================
+--------------------
Coq version 8.4 contains the result of three long-term projects: a new
modular library of arithmetic by Pierre Letouzey, a new proof engine by
@@ -895,7 +899,7 @@ Eelis van der Weegen.
|
Credits: version 8.5
-====================
+--------------------
Coq version 8.5 contains the result of five specific long-term projects:
@@ -1049,7 +1053,7 @@ Tankink. Maxime Dénès coordinated the release process.
|
Credits: version 8.6
-====================
+--------------------
Coq version 8.6 contains the result of refinements, stabilization of
8.5’s features and cleanups of the internals of the system. Over the
@@ -1189,7 +1193,8 @@ Dénès to put together a |Coq| consortium.
|
Credits: version 8.7
-====================
+--------------------
+
|Coq| version 8.7 contains the result of refinements, stabilization of features
and cleanups of the internals of the system along with a few new features. The
main user visible changes are:
@@ -1294,8 +1299,7 @@ system, is now upcoming and will rely on Inria’s newly created Foundation.
|
Credits: version 8.8
-====================
-
+--------------------
|Coq| version 8.8 contains the result of refinements and stabilization of
features and deprecations, cleanups of the internals of the system along
diff --git a/doc/sphinx/index.html.rst b/doc/sphinx/index.html.rst
index cf12b57414..a652b9e1ca 100644
--- a/doc/sphinx/index.html.rst
+++ b/doc/sphinx/index.html.rst
@@ -1,13 +1,11 @@
-.. _introduction:
-
==========================
-Introduction
+Introduction and Contents
==========================
.. include:: introduction.rst
-Table of contents
------------------
+Contents
+--------
.. toctree::
:caption: Indexes
@@ -82,9 +80,6 @@ Table of contents
zebibliography
-License
--------
-
.. include:: license.rst
.. [#PG] Proof-General is available at https://proofgeneral.github.io/.
diff --git a/doc/sphinx/index.latex.rst b/doc/sphinx/index.latex.rst
index af757f8746..9e9eb330fe 100644
--- a/doc/sphinx/index.latex.rst
+++ b/doc/sphinx/index.latex.rst
@@ -2,26 +2,22 @@
The Coq Reference Manual
==========================
+------------
Introduction
------------
.. include:: introduction.rst
+.. include:: license.rst
+
.. [#PG] Proof-General is available at https://proofgeneral.github.io/.
Optionally, you can enhance it with the minor mode
Company-Coq :cite:`Pit16`
(see https://github.com/cpitclaudel/company-coq).
-Credits
--------
-
.. include:: credits.rst
-License
--------
-
-.. include:: license.rst
-
+------------
The language
------------
@@ -33,6 +29,7 @@ The language
language/cic
language/module-system
+----------------
The proof engine
----------------
@@ -45,6 +42,7 @@ The proof engine
proof-engine/detailed-tactic-examples
proof-engine/ssreflect-proof-language
+---------------
User extensions
---------------
@@ -53,6 +51,7 @@ User extensions
user-extensions/syntax-extensions
user-extensions/proof-schemes
+---------------
Practical tools
---------------
@@ -62,6 +61,7 @@ Practical tools
practical-tools/utilities
practical-tools/coqide
+--------
Addendum
--------
diff --git a/doc/sphinx/introduction.rst b/doc/sphinx/introduction.rst
index 5bb7bf542c..bcdf3277ad 100644
--- a/doc/sphinx/introduction.rst
+++ b/doc/sphinx/introduction.rst
@@ -44,7 +44,7 @@ are processed from a file.
.. seealso:: :ref:`thecoqcommands`.
How to read this book
-=====================
+---------------------
This is a Reference Manual, so it is not intended for continuous reading.
We recommend using the various indexes to quickly locate the documentation
@@ -90,7 +90,7 @@ Nonetheless, the manual has some structure that is explained below.
solvers and tactics. See the table of contents for a complete list.
List of additional documentation
-================================
+--------------------------------
This manual does not contain all the documentation the user may need
about |Coq|. Various informations can be found in the following documents:
diff --git a/doc/sphinx/license.rst b/doc/sphinx/license.rst
index 232b04211c..55c6d988f0 100644
--- a/doc/sphinx/license.rst
+++ b/doc/sphinx/license.rst
@@ -1,3 +1,6 @@
+License
+-------
+
This material (the Coq 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
diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst
index 19995520bb..7c78e1a50f 100644
--- a/doc/sphinx/practical-tools/utilities.rst
+++ b/doc/sphinx/practical-tools/utilities.rst
@@ -41,15 +41,17 @@ Building a |Coq| project with coq_makefile
The majority of |Coq| projects are very similar: a collection of ``.v``
files and eventually some ``.ml`` ones (a |Coq| plugin). The main piece of
metadata needed in order to build the project are the command line
-options to ``coqc`` (e.g. ``-R``, ``-I``, see also: section
-:ref:`command-line-options`). Collecting the list of files and options is the job
-of the ``_CoqProject`` file.
+options to ``coqc`` (e.g. ``-R``, ``Q``, ``-I``, see :ref:`command
+line options <command-line-options>`). Collecting the list of files
+and options is the job of the ``_CoqProject`` file.
A simple example of a ``_CoqProject`` file follows:
::
-R theories/ MyCode
+ -arg -w
+ -arg all
theories/foo.v
theories/bar.v
-I src/
@@ -57,6 +59,11 @@ A simple example of a ``_CoqProject`` file follows:
src/bazaux.ml
src/qux_plugin.mlpack
+where options ``-R``, ``-Q`` and ``-I`` are natively recognized, as well as
+file names. The lines of the form ``-arg foo`` are used in order to tell
+to literally pass an argument ``foo`` to ``coqc``: in the
+example, this allows to pass the two-word option ``-w all`` (see
+:ref:`command line options <command-line-options>`).
Currently, both |CoqIDE| and Proof-General (version ≥ ``4.3pre``)
understand ``_CoqProject`` files and invoke |Coq| with the desired options.
diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst
index 46851050ac..c802f44ac1 100644
--- a/doc/sphinx/proof-engine/proof-handling.rst
+++ b/doc/sphinx/proof-engine/proof-handling.rst
@@ -632,16 +632,15 @@ How to enable diffs
```````````````````
.. opt:: Diffs %( "on" %| "off" %| "removed" %)
+ :name: Diffs
- .. This ref doesn't work: :opt:`Set Diffs %( "on" %| "off" %| "removed" %)`
-
- The “on” option highlights added tokens in green, while the “removed” option
- additionally reprints items with removed tokens in red. Unchanged tokens in
- modified items are shown with pale green or red. (Colors are user-configurable.)
+ The “on” option highlights added tokens in green, while the “removed” option
+ additionally reprints items with removed tokens in red. Unchanged tokens in
+ modified items are shown with pale green or red. (Colors are user-configurable.)
For coqtop, showing diffs can be enabled when starting coqtop with the
-``-diffs on|off|removed`` command-line option or with the ``Set Diffs``
-command within Coq. You will need to provide the ``-color on|auto`` command-line option when
+``-diffs on|off|removed`` command-line option or by setting the :opt:`Diffs` option
+within Coq. You will need to provide the ``-color on|auto`` command-line option when
you start coqtop in either case.
Colors for coqtop can be configured by setting the ``COQ_COLORS`` environment
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index db9f04ba11..794804a1f6 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -3513,6 +3513,7 @@ The general command to add a hint to some databases :n:`{+ @ident}` is
Info 1 auto with eqdec.
.. cmdv:: Hint Cut @regexp
+ :name: Hint Cut
.. warning::
@@ -3546,6 +3547,7 @@ The general command to add a hint to some databases :n:`{+ @ident}` is
initial cut expression being `emp`.
.. cmdv:: Hint Mode @qualid {* (+ | ! | -)}
+ :name: Hint Mode
This sets an optional mode of use of the identifier :n:`@qualid`. When
proof-search faces a goal that ends in an application of :n:`@qualid` to
diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst
index 125c4c25a3..a69cf209c7 100644
--- a/doc/sphinx/proof-engine/vernacular-commands.rst
+++ b/doc/sphinx/proof-engine/vernacular-commands.rst
@@ -461,6 +461,7 @@ Requests to the environment
.. note::
.. table:: Search Blacklist @string
+ :name: Search Blacklist
Specifies a set of strings used to exclude lemmas from the results of :cmd:`Search`,
:cmd:`SearchHead`, :cmd:`SearchPattern` and :cmd:`SearchRewrite` queries. A lemma whose
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 14:07:20 +0000