aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--CHANGES10
-rw-r--r--Makefile.doc6
-rw-r--r--configure.ml24
-rw-r--r--dev/build/windows/MakeCoq_86_abs_ocaml.bat10
-rw-r--r--dev/build/windows/MakeCoq_86_installer.bat8
-rw-r--r--dev/build/windows/MakeCoq_86_installer_32.bat8
-rw-r--r--dev/build/windows/MakeCoq_86beta1_abs_ocaml.bat10
-rw-r--r--dev/build/windows/MakeCoq_86beta1_installer.bat8
-rw-r--r--dev/build/windows/MakeCoq_86beta1_installer_32.bat8
-rw-r--r--dev/build/windows/MakeCoq_86rc1_abs_ocaml.bat10
-rw-r--r--dev/build/windows/MakeCoq_86rc1_installer.bat8
-rw-r--r--dev/build/windows/MakeCoq_86rc1_installer_32.bat8
-rw-r--r--doc/refman/RefMan-syn.tex2
-rw-r--r--doc/tutorial/Tutorial.tex61
-rw-r--r--ide/ide_slave.ml3
-rw-r--r--kernel/byterun/coq_interp.c63
-rw-r--r--kernel/pre_env.ml3
-rw-r--r--lib/aux_file.ml4
-rw-r--r--lib/system.ml7
-rw-r--r--plugins/ssrmatching/ssrmatching.ml411
-rw-r--r--stm/stm.ml6
-rw-r--r--tools/coq_makefile.ml2
-rw-r--r--toplevel/vernacentries.ml6
23 files changed, 215 insertions, 71 deletions
diff --git a/CHANGES b/CHANGES
index 090f7c13b..4a7cb8c45 100644
--- a/CHANGES
+++ b/CHANGES
@@ -7,6 +7,16 @@ Tactics
functional extensionality in H supposed to be a quantified equality
until giving a bare equality.
+Changes from V8.6beta1 to V8.6
+==============================
+
+Kernel
+
+- Fixed critical bug #5248 in VM long multiplication on 32-bit
+ architectures. Was there only since 8.6beta1, so no stable release impacted.
+
+Other bug fixes in universes, type class shelving,...
+
Changes from V8.5 to V8.6beta1
==============================
diff --git a/Makefile.doc b/Makefile.doc
index cdd9852e8..9ae20ba76 100644
--- a/Makefile.doc
+++ b/Makefile.doc
@@ -201,15 +201,17 @@ doc/refman/styles.hva: doc/common/styles/html/$(HTMLSTYLE)/styles.hva
$(INSTALLLIB) $< doc/refman
INDEXES:= doc/refman/html/command-index.html doc/refman/html/tactic-index.html
-ALLINDEXES:= doc/refman/html/index.html $(INDEXES)
-refman-html-dir $(ALLINDEXES): doc/refman/Reference-Manual.html $(REFMANPNGFILES) \
+refman-html-dir $(INDEXES): doc/refman/html/index.html ;
+
+doc/refman/html/index.html: doc/refman/Reference-Manual.html $(REFMANPNGFILES) \
doc/refman/cover.html doc/refman/styles.hva doc/refman/index.html
- rm -rf doc/refman/html
$(MKDIR) doc/refman/html
$(INSTALLLIB) $(REFMANPNGFILES) doc/refman/html
(cd doc/refman/html; $(HACHA) -nolinks -tocbis -o toc.html ../styles.hva ../Reference-Manual.html)
$(INSTALLLIB) doc/refman/cover.html doc/refman/html/index.html
+ @touch $(INDEXES)
-$(INSTALLLIB) doc/common/styles/html/$(HTMLSTYLE)/*.css doc/refman/html
refman-quick:
diff --git a/configure.ml b/configure.ml
index f75bbb538..48e167c99 100644
--- a/configure.ml
+++ b/configure.ml
@@ -12,10 +12,10 @@
open Printf
let coq_version = "trunk"
-let coq_macos_version = "8.4.90" (** "[...] should be a string comprised of
+let coq_macos_version = "8.6.90" (** "[...] should be a string comprised of
three non-negative, period-separated integers [...]" *)
-let vo_magic = 8591
-let state_magic = 58591
+let vo_magic = 8691
+let state_magic = 58691
let distributed_exec = ["coqtop";"coqc";"coqchk";"coqdoc";"coqmktop";"coqworkmgr";
"coqdoc";"coq_makefile";"coq-tex";"gallina";"coqwc";"csdpcert";"coqdep"]
@@ -509,6 +509,20 @@ let camltag = match caml_version_list with
(** * CamlpX configuration *)
(* Convention: we use camldir as a prioritary location for camlpX, if given *)
+(* i.e., in the case of camlp5, we search for a copy of camlp5o which *)
+(* answers the right camlp5 lib dir *)
+
+let strip_slash dir =
+ let n = String.length dir in
+ if n>0 && dir.[n - 1] = '/' then String.sub dir 0 (n-1) else dir
+
+let which_camlp5o_for camlp5lib =
+ let camlp5o = Filename.concat camlbin "camlp5o" in
+ let camlp5lib = strip_slash camlp5lib in
+ if fst (tryrun camlp5o ["-where"]) = camlp5lib then camlp5o else
+ let camlp5o = which "camlp5o" in
+ if fst (tryrun camlp5o ["-where"]) = camlp5lib then camlp5o else
+ die ("Error: cannot find Camlp5 binaries corresponding to Camlp5 library " ^ camlp5lib)
let which_camlpX base =
let file = Filename.concat camlbin base in
@@ -523,7 +537,7 @@ let check_camlp5 testcma = match !Prefs.camlp5dir with
| Some dir ->
if Sys.file_exists (dir/testcma) then
let camlp5o =
- try which_camlpX "camlp5o"
+ try which_camlp5o_for dir
with Not_found -> die "Error: cannot find Camlp5 binaries in path.\n" in
dir, camlp5o
else
@@ -544,7 +558,7 @@ let check_camlp5 testcma = match !Prefs.camlp5dir with
let check_camlp5_version camlp5o =
let version_line, _ = run ~err:StdOut camlp5o ["-v"] in
let version = List.nth (string_split ' ' version_line) 2 in
- match string_split '.' version with
+ match numeric_prefix_list version with
| major::minor::_ when s2i major > 6 || (s2i major, s2i minor) >= (6,6) ->
printf "You have Camlp5 %s. Good!\n" version; version
| _ -> die "Error: unsupported Camlp5 (version < 6.06 or unrecognized).\n"
diff --git a/dev/build/windows/MakeCoq_86_abs_ocaml.bat b/dev/build/windows/MakeCoq_86_abs_ocaml.bat
new file mode 100644
index 000000000..50483c4d4
--- /dev/null
+++ b/dev/build/windows/MakeCoq_86_abs_ocaml.bat
@@ -0,0 +1,10 @@
+call MakeCoq_SetRootPath
+
+call MakeCoq_MinGW.bat ^
+ -arch=64 ^
+ -mode=absolute ^
+ -ocaml=Y ^
+ -make=Y ^
+ -coqver=8.6 ^
+ -destcyg=%ROOTPATH%\cygwin_coq64_86_abs ^
+ -destcoq=%ROOTPATH%\coq64_86_abs
diff --git a/dev/build/windows/MakeCoq_86_installer.bat b/dev/build/windows/MakeCoq_86_installer.bat
new file mode 100644
index 000000000..263520ff1
--- /dev/null
+++ b/dev/build/windows/MakeCoq_86_installer.bat
@@ -0,0 +1,8 @@
+call MakeCoq_SetRootPath
+
+call MakeCoq_MinGW.bat ^
+ -arch=64 ^
+ -installer=Y ^
+ -coqver=8.6 ^
+ -destcyg=%ROOTPATH%\cygwin_coq64_86_inst ^
+ -destcoq=%ROOTPATH%\coq64_86_inst
diff --git a/dev/build/windows/MakeCoq_86_installer_32.bat b/dev/build/windows/MakeCoq_86_installer_32.bat
new file mode 100644
index 000000000..14921dd7c
--- /dev/null
+++ b/dev/build/windows/MakeCoq_86_installer_32.bat
@@ -0,0 +1,8 @@
+call MakeCoq_SetRootPath
+
+call MakeCoq_MinGW.bat ^
+ -arch=32 ^
+ -installer=Y ^
+ -coqver=8.6 ^
+ -destcyg=%ROOTPATH%\cygwin_coq32_86_inst ^
+ -destcoq=%ROOTPATH%\coq32_86_inst
diff --git a/dev/build/windows/MakeCoq_86beta1_abs_ocaml.bat b/dev/build/windows/MakeCoq_86beta1_abs_ocaml.bat
new file mode 100644
index 000000000..914c332f4
--- /dev/null
+++ b/dev/build/windows/MakeCoq_86beta1_abs_ocaml.bat
@@ -0,0 +1,10 @@
+call MakeCoq_SetRootPath
+
+call MakeCoq_MinGW.bat ^
+ -arch=64 ^
+ -mode=absolute ^
+ -ocaml=Y ^
+ -make=Y ^
+ -coqver=8.6beta1 ^
+ -destcyg=%ROOTPATH%\cygwin_coq64_86beta1_abs ^
+ -destcoq=%ROOTPATH%\coq64_86beta1_abs
diff --git a/dev/build/windows/MakeCoq_86beta1_installer.bat b/dev/build/windows/MakeCoq_86beta1_installer.bat
new file mode 100644
index 000000000..76a5bb35a
--- /dev/null
+++ b/dev/build/windows/MakeCoq_86beta1_installer.bat
@@ -0,0 +1,8 @@
+call MakeCoq_SetRootPath
+
+call MakeCoq_MinGW.bat ^
+ -arch=64 ^
+ -installer=Y ^
+ -coqver=8.6beta1 ^
+ -destcyg=%ROOTPATH%\cygwin_coq64_86beta1_inst ^
+ -destcoq=%ROOTPATH%\coq64_86beta1_inst
diff --git a/dev/build/windows/MakeCoq_86beta1_installer_32.bat b/dev/build/windows/MakeCoq_86beta1_installer_32.bat
new file mode 100644
index 000000000..f53232b65
--- /dev/null
+++ b/dev/build/windows/MakeCoq_86beta1_installer_32.bat
@@ -0,0 +1,8 @@
+call MakeCoq_SetRootPath
+
+call MakeCoq_MinGW.bat ^
+ -arch=32 ^
+ -installer=Y ^
+ -coqver=8.6beta1 ^
+ -destcyg=%ROOTPATH%\cygwin_coq32_86beta1_inst ^
+ -destcoq=%ROOTPATH%\coq32_86beta1_inst
diff --git a/dev/build/windows/MakeCoq_86rc1_abs_ocaml.bat b/dev/build/windows/MakeCoq_86rc1_abs_ocaml.bat
new file mode 100644
index 000000000..c0669f01d
--- /dev/null
+++ b/dev/build/windows/MakeCoq_86rc1_abs_ocaml.bat
@@ -0,0 +1,10 @@
+call MakeCoq_SetRootPath
+
+call MakeCoq_MinGW.bat ^
+ -arch=64 ^
+ -mode=absolute ^
+ -ocaml=Y ^
+ -make=Y ^
+ -coqver=8.6rc1 ^
+ -destcyg=%ROOTPATH%\cygwin_coq64_86rc1_abs ^
+ -destcoq=%ROOTPATH%\coq64_86rc1_abs
diff --git a/dev/build/windows/MakeCoq_86rc1_installer.bat b/dev/build/windows/MakeCoq_86rc1_installer.bat
new file mode 100644
index 000000000..66234ebbd
--- /dev/null
+++ b/dev/build/windows/MakeCoq_86rc1_installer.bat
@@ -0,0 +1,8 @@
+call MakeCoq_SetRootPath
+
+call MakeCoq_MinGW.bat ^
+ -arch=64 ^
+ -installer=Y ^
+ -coqver=8.6rc1 ^
+ -destcyg=%ROOTPATH%\cygwin_coq64_86rc1_inst ^
+ -destcoq=%ROOTPATH%\coq64_86rc1_inst
diff --git a/dev/build/windows/MakeCoq_86rc1_installer_32.bat b/dev/build/windows/MakeCoq_86rc1_installer_32.bat
new file mode 100644
index 000000000..96f43e16a
--- /dev/null
+++ b/dev/build/windows/MakeCoq_86rc1_installer_32.bat
@@ -0,0 +1,8 @@
+call MakeCoq_SetRootPath
+
+call MakeCoq_MinGW.bat ^
+ -arch=32 ^
+ -installer=Y ^
+ -coqver=8.6rc1 ^
+ -destcyg=%ROOTPATH%\cygwin_coq32_86rc1_inst ^
+ -destcoq=%ROOTPATH%\coq32_86rc1_inst
diff --git a/doc/refman/RefMan-syn.tex b/doc/refman/RefMan-syn.tex
index 1fcc1c0df..21c39de96 100644
--- a/doc/refman/RefMan-syn.tex
+++ b/doc/refman/RefMan-syn.tex
@@ -649,7 +649,7 @@ A recursive pattern for binders can be used in position of a recursive
pattern for terms. Here is an example:
\begin{coq_example*}
-Notation ``'FUNAPP' x .. y , f'' :=
+Notation "'FUNAPP' x .. y , f" :=
(fun x => .. (fun y => (.. (f x) ..) y ) ..)
(at level 200, x binder, y binder, right associativity).
\end{coq_example*}
diff --git a/doc/tutorial/Tutorial.tex b/doc/tutorial/Tutorial.tex
index 973a0b75e..0d537256b 100644
--- a/doc/tutorial/Tutorial.tex
+++ b/doc/tutorial/Tutorial.tex
@@ -3,6 +3,7 @@
\usepackage[utf8]{inputenc}
\usepackage{textcomp}
\usepackage{pslatex}
+\usepackage{hyperref}
\input{../common/version.tex}
\input{../common/macros.tex}
@@ -17,7 +18,7 @@
\chapter*{Getting started}
-\Coq\ is a Proof Assistant for a Logical Framework known as the Calculus
+\Coq{} is a Proof Assistant for a Logical Framework known as the Calculus
of Inductive Constructions. It allows the interactive construction of
formal proofs, and also the manipulation of functional programs
consistently with their specifications. It runs as a computer program
@@ -29,7 +30,7 @@ possibilities of \Coq, but rather to present in the most elementary
manner a tutorial on the basic specification language, called Gallina,
in which formal axiomatisations may be developed, and on the main
proof tools. For more advanced information, the reader could refer to
-the \Coq{} Reference Manual or the \textit{Coq'Art}, a new book by Y.
+the \Coq{} Reference Manual or the \textit{Coq'Art}, a book by Y.
Bertot and P. Castéran on practical uses of the \Coq{} system.
Coq can be used from a standard teletype-like shell window but
@@ -39,9 +40,9 @@ and Pcoq.}.
Instructions on installation procedures, as well as more comprehensive
documentation, may be found in the standard distribution of \Coq,
-which may be obtained from \Coq{} web site \texttt{http://coq.inria.fr}.
+which may be obtained from \Coq{} web site \url{https://coq.inria.fr/}.
-In the following, we assume that \Coq~ is called from a standard
+In the following, we assume that \Coq{} is called from a standard
teletype-like shell window. All examples preceded by the prompting
sequence \verb:Coq < : represent user input, terminated by a
period.
@@ -51,10 +52,10 @@ users screen. When used from a graphical user interface such as
CoqIde, the prompt is not displayed: user input is given in one window
and \Coq's answers are displayed in a different window.
-The sequence of such examples is a valid \Coq~
+The sequence of such examples is a valid \Coq{}
session, unless otherwise specified. This version of the tutorial has
been prepared on a PC workstation running Linux. The standard
-invocation of \Coq\ delivers a message such as:
+invocation of \Coq{} delivers a message such as:
\begin{small}
\begin{flushleft}
@@ -67,17 +68,17 @@ Coq <
\end{flushleft}
\end{small}
-The first line gives a banner stating the precise version of \Coq~
+The first line gives a banner stating the precise version of \Coq{}
used. You should always return this banner when you report an anomaly
to our bug-tracking system
-\verb|http://logical.futurs.inria.fr/coq-bugs|
+\url{https://coq.inria.fr/bugs/}.
\chapter{Basic Predicate Calculus}
\section{An overview of the specification language Gallina}
A formal development in Gallina consists in a sequence of {\sl declarations}
-and {\sl definitions}. You may also send \Coq~ {\sl commands} which are
+and {\sl definitions}. You may also send \Coq{} {\sl commands} which are
not really part of the formal development, but correspond to information
requests, or service routine invocations. For instance, the command:
\begin{verbatim}
@@ -106,7 +107,7 @@ of the system, called respectively \verb:Prop:, \verb:Set:, and
Every valid expression $e$ in Gallina is associated with a specification,
itself a valid expression, called its {\sl type} $\tau(E)$. We write
$e:\tau(E)$ for the judgment that $e$ is of type $E$.
-You may request \Coq~ to return to you the type of a valid expression by using
+You may request \Coq{} to return to you the type of a valid expression by using
the command \verb:Check::
\begin{coq_eval}
@@ -130,7 +131,7 @@ Check nat.
The specification \verb:Set: is an abstract type, one of the basic
sorts of the Gallina language, whereas the notions $nat$ and $O$ are
notions which are defined in the arithmetic prelude,
-automatically loaded when running the \Coq\ system.
+automatically loaded when running the \Coq{} system.
We start by introducing a so-called section name. The role of sections
is to structure the modelisation by limiting the scope of parameters,
@@ -206,7 +207,7 @@ We may optionally indicate the required type:
Definition two : nat := S one.
\end{coq_example}
-Actually \Coq~ allows several possible syntaxes:
+Actually \Coq{} allows several possible syntaxes:
\begin{coq_example}
Definition three := S two : nat.
\end{coq_example}
@@ -249,7 +250,7 @@ explicitly the type of the quantified variable. We check:
Check (forall m:nat, gt m 0).
\end{coq_example}
We may revert to the clean state of
-our initial session using the \Coq~ \verb:Reset: command:
+our initial session using the \Coq{} \verb:Reset: command:
\begin{coq_example}
Reset Initial.
\end{coq_example}
@@ -340,7 +341,7 @@ assumption.
\end{coq_example}
The proof is now finished. We may either discard it, by using the
-command \verb:Abort: which returns to the standard \Coq~ toplevel loop
+command \verb:Abort: which returns to the standard \Coq{} toplevel loop
without further ado, or else save it as a lemma in the current context,
under name say \verb:trivial_lemma::
\begin{coq_example}
@@ -414,7 +415,7 @@ backtrack one step, and more generally \verb:Undo n: to
backtrack n steps.
We end this section by showing a useful command, \verb:Inspect n.:,
-which inspects the global \Coq~ environment, showing the last \verb:n: declared
+which inspects the global \Coq{} environment, showing the last \verb:n: declared
notions:
\begin{coq_example}
Inspect 3.
@@ -429,7 +430,7 @@ their value (or proof-term) is omitted.
\subsection{Conjunction}
We have seen how \verb:intro: and \verb:apply: tactics could be combined
-in order to prove implicational statements. More generally, \Coq~ favors a style
+in order to prove implicational statements. More generally, \Coq{} favors a style
of reasoning, called {\sl Natural Deduction}, which decomposes reasoning into
so called {\sl introduction rules}, which tell how to prove a goal whose main
operator is a given propositional connective, and {\sl elimination rules},
@@ -528,7 +529,7 @@ such a simple tautology. The reason is that we want to keep
\subsection{Tauto}
A complete tactic for propositional
-tautologies is indeed available in \Coq~ as the \verb:tauto: tactic.
+tautologies is indeed available in \Coq{} as the \verb:tauto: tactic.
\begin{coq_example}
Restart.
tauto.
@@ -555,7 +556,7 @@ The two instantiations are effected automatically by the tactic
\verb:apply: when pattern-matching a goal. The specialist will of course
recognize our proof term as a $\lambda$-term, used as notation for the
natural deduction proof term through the Curry-Howard isomorphism. The
-naive user of \Coq~ may safely ignore these formal details.
+naive user of \Coq{} may safely ignore these formal details.
Let us exercise the \verb:tauto: tactic on a more complex example:
\begin{coq_example}
@@ -579,7 +580,7 @@ argument fails.
This may come as a surprise to someone familiar with classical reasoning.
Peirce's lemma is true in Boolean logic, i.e. it evaluates to \verb:true: for
every truth-assignment to \verb:A: and \verb:B:. Indeed the double negation
-of Peirce's law may be proved in \Coq~ using \verb:tauto::
+of Peirce's law may be proved in \Coq{} using \verb:tauto::
\begin{coq_example}
Abort.
Lemma NNPeirce : ~ ~ (((A -> B) -> A) -> A).
@@ -588,7 +589,7 @@ Qed.
\end{coq_example}
In classical logic, the double negation of a proposition is equivalent to this
-proposition, but in the constructive logic of \Coq~ this is not so. If you
+proposition, but in the constructive logic of \Coq{} this is not so. If you
want to use classical logic in \Coq, you have to import explicitly the
\verb:Classical: module, which will declare the axiom \verb:classic:
of excluded middle, and classical tautologies such as de Morgan's laws.
@@ -652,7 +653,7 @@ function and predicate symbols.
\subsection{Sections and signatures}
Usually one works in some domain of discourse, over which range the individual
-variables and function symbols. In \Coq~ we speak in a language with a rich
+variables and function symbols. In \Coq{} we speak in a language with a rich
variety of types, so me may mix several domains of discourse, in our
multi-sorted language. For the moment, we just do a few exercises, over a
domain of discourse \verb:D: axiomatised as a \verb:Set:, and we consider two
@@ -660,7 +661,7 @@ predicate symbols \verb:P: and \verb:R: over \verb:D:, of arities
respectively 1 and 2. Such abstract entities may be entered in the context
as global variables. But we must be careful about the pollution of our
global environment by such declarations. For instance, we have already
-polluted our \Coq~ session by declaring the variables
+polluted our \Coq{} session by declaring the variables
\verb:n:, \verb:Pos_n:, \verb:A:, \verb:B:, and \verb:C:.
\begin{coq_example}
@@ -714,7 +715,7 @@ Check ex.
\end{coq_example}
and the notation \verb+(exists x:D, P x)+ is just concrete syntax for
the expression \verb+(ex D (fun x:D => P x))+.
-Existential quantification is handled in \Coq~ in a similar
+Existential quantification is handled in \Coq{} in a similar
fashion to the connectives \verb:/\: and \verb:\/: : it is introduced by
the proof combinator \verb:ex_intro:, which is invoked by the specific
tactic \verb:Exists:, and its elimination provides a witness \verb+a:D+ to
@@ -951,7 +952,7 @@ Abort.
\subsection{Equality}
-The basic equality provided in \Coq~ is Leibniz equality, noted infix like
+The basic equality provided in \Coq{} is Leibniz equality, noted infix like
\verb+x=y+, when \verb:x: and \verb:y: are two expressions of
type the same Set. The replacement of \verb:x: by \verb:y: in any
term is effected by a variety of tactics, such as \verb:rewrite:
@@ -1208,7 +1209,7 @@ About prim_rec.
Oops! Instead of the expected type \verb+nat->(nat->nat->nat)->nat->nat+ we
get an apparently more complicated expression. Indeed the type of
\verb:prim_rec: is equivalent by rule $\beta$ to its expected type; this may
-be checked in \Coq~ by command \verb:Eval Cbv Beta:, which $\beta$-reduces
+be checked in \Coq{} by command \verb:Eval Cbv Beta:, which $\beta$-reduces
an expression to its {\sl normal form}:
\begin{coq_example}
Eval cbv beta in
@@ -1228,7 +1229,7 @@ That is, we specify that \verb+(addition n m)+ computes by cases on \verb:n:
according to its main constructor; when \verb:n = O:, we get \verb:m:;
when \verb:n = S p:, we get \verb:(S rec):, where \verb:rec: is the result
of the recursive computation \verb+(addition p m)+. Let us verify it by
-asking \Coq~to compute for us say $2+3$:
+asking \Coq{} to compute for us say $2+3$:
\begin{coq_example}
Eval compute in (addition (S (S O)) (S (S (S O)))).
\end{coq_example}
@@ -1275,7 +1276,7 @@ as subgoals the corresponding instantiations of the base case \verb:(P O): ,
and of the inductive step \verb+forall y:nat, P y -> P (S y)+.
In each case we get an instance of function \verb:plus: in which its second
argument starts with a constructor, and is thus amenable to simplification
-by primitive recursion. The \Coq~tactic \verb:simpl: can be used for
+by primitive recursion. The \Coq{} tactic \verb:simpl: can be used for
this purpose:
\begin{coq_example}
simpl.
@@ -1488,7 +1489,7 @@ Set Printing Width 60.
\section{Opening library modules}
-When you start \Coq~ without further requirements in the command line,
+When you start \Coq{} without further requirements in the command line,
you get a bare system with few libraries loaded. As we saw, a standard
prelude module provides the standard logic connectives, and a few
arithmetic notions. If you want to load and open other modules from
@@ -1503,9 +1504,9 @@ Such a command looks for a (compiled) module file \verb:Arith.vo: in
the libraries registered by \Coq. Libraries inherit the structure of
the file system of the operating system and are registered with the
command \verb:Add LoadPath:. Physical directories are mapped to
-logical directories. Especially the standard library of \Coq~ is
+logical directories. Especially the standard library of \Coq{} is
pre-registered as a library of name \verb=Coq=. Modules have absolute
-unique names denoting their place in \Coq~ libraries. An absolute
+unique names denoting their place in \Coq{} libraries. An absolute
name is a sequence of single identifiers separated by dots. E.g. the
module \verb=Arith= has full name \verb=Coq.Arith.Arith= and because
it resides in eponym subdirectory \verb=Arith= of the standard
diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml
index 48fd0a93e..ae3dcd94a 100644
--- a/ide/ide_slave.ml
+++ b/ide/ide_slave.ml
@@ -393,7 +393,8 @@ let init =
Stm.add false ~ontop:(Stm.get_current_state ())
0 (Printf.sprintf "Add LoadPath \"%s\". " dir)
else Stm.get_current_state (), `NewTip in
- Stm.set_compilation_hints file;
+ if Filename.check_suffix file ".v" then
+ Stm.set_compilation_hints file;
Stm.finish ();
initial_id
end
diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index 5dec3b785..af89712d5 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -891,25 +891,58 @@ value coq_interprete
Instruct(PROJ){
+ do_proj:
print_instr("PROJ");
if (Is_accu (accu)) {
- value block;
- /* Skip over the index of projected field */
- pc++;
- /* Create atom */
- Alloc_small(block, 2, ATOM_PROJ_TAG);
- Field(block, 0) = Field(coq_global_data, *pc);
- Field(block, 1) = accu;
- accu = block;
- /* Create accumulator */
- Alloc_small(block, 2, Accu_tag);
- Code_val(block) = accumulate;
- Field(block, 1) = accu;
- accu = block;
+ *--sp = accu; // Save matched block on stack
+ accu = Field(accu, 1); // Save atom to accu register
+ switch (Tag_val(accu)) {
+ case ATOM_COFIX_TAG: // We are forcing a cofix
+ {
+ mlsize_t i, nargs;
+ sp -= 2;
+ // Push the current instruction as the return address
+ sp[0] = (value)(pc - 1);
+ sp[1] = coq_env;
+ coq_env = Field(accu, 0); // Pointer to suspension
+ accu = sp[2]; // Save accumulator to accu register
+ sp[2] = Val_long(coq_extra_args); // Push number of args for return
+ nargs = Wosize_val(accu) - 2; // Number of args = size of accumulator - 1 (accumulator code) - 1 (atom)
+ // Push arguments to stack
+ CHECK_STACK(nargs + 1);
+ sp -= nargs;
+ for (i = 0; i < nargs; ++i) sp[i] = Field(accu, i + 2);
+ *--sp = accu; // Last argument is the pointer to the suspension
+ coq_extra_args = nargs;
+ pc = Code_val(coq_env); // Trigger evaluation
+ goto check_stack;
+ }
+ case ATOM_COFIXEVALUATED_TAG:
+ {
+ accu = Field(accu, 1);
+ ++sp;
+ goto do_proj;
+ }
+ default:
+ {
+ value block;
+ /* Skip over the index of projected field */
+ ++pc;
+ /* Create atom */
+ Alloc_small(accu, 2, ATOM_PROJ_TAG);
+ Field(accu, 0) = Field(coq_global_data, *pc++);
+ Field(accu, 1) = *sp++;
+ /* Create accumulator */
+ Alloc_small(block, 2, Accu_tag);
+ Code_val(block) = accumulate;
+ Field(block, 1) = accu;
+ accu = block;
+ }
+ }
} else {
- accu = Field(accu, *pc++);
+ accu = Field(accu, *pc);
+ pc += 2;
}
- pc++;
Next;
}
diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml
index 72de2f1a6..d14a254d3 100644
--- a/kernel/pre_env.ml
+++ b/kernel/pre_env.ml
@@ -157,7 +157,8 @@ let map_named_val f ctxt =
(accu, d')
in
let map, ctx = List.fold_map fold ctxt.env_named_map ctxt.env_named_ctx in
- { env_named_ctx = ctx; env_named_map = map }
+ if map == ctxt.env_named_map then ctxt
+ else { env_named_ctx = ctx; env_named_map = map }
let push_named d env =
(* if not (env.env_rel_context = []) then raise (ASSERT env.env_rel_context);
diff --git a/lib/aux_file.ml b/lib/aux_file.ml
index 17f55330d..1b6651a55 100644
--- a/lib/aux_file.ml
+++ b/lib/aux_file.ml
@@ -17,10 +17,6 @@ let version = 1
let oc = ref None
-let chop_extension f =
- if check_suffix f ".v" then chop_extension f
- else f
-
let aux_file_name_for vfile =
dirname vfile ^ "/." ^ chop_extension(basename vfile) ^ ".aux"
diff --git a/lib/system.ml b/lib/system.ml
index 74dd224a0..e0e2c829d 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -309,6 +309,7 @@ let with_time time f x =
raise e
let process_id () =
- if Flags.async_proofs_is_worker () then !Flags.async_proofs_worker_id
- else Printf.sprintf "master:%d" (Thread.id (Thread.self ()))
-
+ Printf.sprintf "%d:%s:%d" (Unix.getpid ())
+ (if Flags.async_proofs_is_worker () then !Flags.async_proofs_worker_id
+ else "master")
+ (Thread.id (Thread.self ()))
diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4
index 0d4be72d9..fc988a2c5 100644
--- a/plugins/ssrmatching/ssrmatching.ml4
+++ b/plugins/ssrmatching/ssrmatching.ml4
@@ -391,7 +391,8 @@ let iter_constr_LR f c = match kind_of_term c with
| Case (_, p, v, b) -> f v; f p; Array.iter f b
| Fix (_, (_, t, b)) | CoFix (_, (_, t, b)) ->
for i = 0 to Array.length t - 1 do f t.(i); f b.(i) done
- | _ -> ()
+ | Proj(_,a) -> f a
+ | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ | Construct _) -> ()
(* The comparison used to determine which subterms matches is KEYED *)
(* CONVERSION. This looks for convertible terms that either have the same *)
@@ -525,7 +526,13 @@ let nb_cs_proj_args pc f u =
try match kind_of_term f with
| Prod _ -> na Prod_cs
| Sort s -> na (Sort_cs (family_of_sort s))
- | Const (c',_) when Constant.equal c' pc -> Array.length (snd (destApp u.up_f))
+ | Const (c',_) when Constant.equal c' pc ->
+ begin match kind_of_term u.up_f with
+ | App(_,args) -> Array.length args
+ | Proj _ -> 0 (* if splay_app calls expand_projection, this has to be
+ the number of arguments including the projected *)
+ | _ -> assert false
+ end
| Var _ | Ind _ | Construct _ | Const _ -> na (Const_cs (global_of_constr f))
| _ -> -1
with Not_found -> -1
diff --git a/stm/stm.ml b/stm/stm.ml
index f7569d257..6f34c8dbc 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -2584,12 +2584,12 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty
if not in_proof && Proof_global.there_are_pending_proofs () then
begin
let bname = VCS.mk_branch_name x in
- let opacity_of_produced_term =
- match x.expr with
+ let rec opacity_of_produced_term = function
(* This AST is ambiguous, hence we check it dynamically *)
| VernacInstance (false, _,_ , None, _) -> GuaranteesOpacity
+ | VernacLocal (_,e) -> opacity_of_produced_term e
| _ -> Doesn'tGuaranteeOpacity in
- VCS.commit id (Fork (x,bname,opacity_of_produced_term,[]));
+ VCS.commit id (Fork (x,bname,opacity_of_produced_term x.expr,[]));
let proof_mode = default_proof_mode () in
VCS.branch bname (`Proof (proof_mode, VCS.proof_nesting () + 1));
Proof_global.activate_proof_mode proof_mode;
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index eab909f5b..b7dd5f2a1 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -390,7 +390,7 @@ let clean sds sps =
let () =
if !some_vfile then
let () = print "cleanall:: clean\n" in
- print "\trm -f $(patsubst %.v,.%.aux,$(VFILES))\n\n" in
+ print "\trm -f $(foreach f,$(VFILES:.v=),$(dir $(f)).$(notdir $(f)).aux)\n\n" in
print "archclean::\n";
print "\trm -f *.cmx *.o\n";
List.iter
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 8ce13c69a..a2f2ded32 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -571,10 +571,10 @@ let vernac_inductive poly lo finite indl =
| _ -> () (* dumping is done by vernac_record (called below) *) )
indl;
match indl with
- | [ ( _ , _ , _ ,Record, Constructors _ ),_ ] ->
- CErrors.error "The Record keyword cannot be used to define a variant type. Use Variant instead."
+ | [ ( _ , _ , _ ,(Record|Structure), Constructors _ ),_ ] ->
+ CErrors.error "The Record keyword is for types defined using the syntax { ... }."
| [ (_ , _ , _ ,Variant, RecordDecl _),_ ] ->
- CErrors.error "The Variant keyword cannot be used to define a record type. Use Record instead."
+ CErrors.error "The Variant keyword does not support syntax { ... }."
| [ ( id , bl , c , b, RecordDecl (oc,fs) ), [] ] ->
vernac_record (match b with Class _ -> Class false | _ -> b)
poly finite id bl c oc fs
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-23 11:10:01 +0000