diff options
| -rw-r--r-- | CHANGES | 2 | ||||
| -rw-r--r-- | doc/faq/FAQ.tex | 2 | ||||
| -rw-r--r-- | doc/refman/Micromega.tex | 2 | ||||
| -rw-r--r-- | doc/refman/Setoid.tex | 2 | ||||
| -rw-r--r-- | plugins/extraction/README | 2 | ||||
| -rw-r--r-- | plugins/romega/ReflOmegaCore.v | 4 | ||||
| -rw-r--r-- | theories/FSets/FMapAVL.v | 2 | ||||
| -rw-r--r-- | theories/PArith/BinPosDef.v | 4 |
8 files changed, 10 insertions, 10 deletions
@@ -60,7 +60,7 @@ Vernacular commands Specification Language - Slight changes in unification error messages. -- Added a syntax $(...)$ allowing to put tactics in terms. +- Added a syntax $(...)$ that allows putting tactics in terms. - Constants in pattern-matching branches now respect the same rules regarding implicit arguments than in applicative position. The old behaviour can be recovered by the command "Set Asymmetric Patterns". (possible source of diff --git a/doc/faq/FAQ.tex b/doc/faq/FAQ.tex index 5806e9d72..fba210c69 100644 --- a/doc/faq/FAQ.tex +++ b/doc/faq/FAQ.tex @@ -1644,7 +1644,7 @@ is a strong specification, using the \texttt{sumbool} type (look at the reference manual or chapter 9 of \cite{coqart}). Eliminations of the form ``~\texttt{case (le\_lt\_dec n p)}~'' provide proofs of -either $n \leq p$ or $p < n$, allowing to prove easily theorems as in +either $n \leq p$ or $p < n$, allowing easy proofs of some theorems as in question~\ref{minmax}. Unfortunately, this not the case of your \texttt{my\_le\_lt\_dec}, which returns a quite non-informative boolean value. diff --git a/doc/refman/Micromega.tex b/doc/refman/Micromega.tex index 7bdbd6d84..c9180b40c 100644 --- a/doc/refman/Micromega.tex +++ b/doc/refman/Micromega.tex @@ -15,7 +15,7 @@ The {\tt Psatz} module ({\tt Require Psatz.}) gives access to several tactics fo \item {\tt psatz D n} where {\tt D} is {\tt Z}, {\tt Q} or {\tt R} and {\tt n} is an optional integer limiting the proof search depth is is an incomplete proof procedure for non-linear arithmetic. It is based on John Harrison's Hol light driver to the external prover {\tt cspd}\footnote{Sources and binaries can be found at \url{https://projects.coin-or.org/Csdp}}. Note that the {\tt csdp} driver is generating - a \emph{proof cache} thus allowing to rerun scripts even without {\tt csdp} (see Section~\ref{sec:psatz}). + a \emph{proof cache} which allows rerunning scripts even without {\tt csdp} (see Section~\ref{sec:psatz}). \end{itemize} The tactics solve propositional formulas parameterised by atomic arithmetics expressions diff --git a/doc/refman/Setoid.tex b/doc/refman/Setoid.tex index 55915189c..ca416d7b1 100644 --- a/doc/refman/Setoid.tex +++ b/doc/refman/Setoid.tex @@ -9,7 +9,7 @@ to work over user-defined structures (called setoids) that are equipped with ad-hoc equivalence relations meant to behave as equalities. Actually, the tactics have also been generalized to relations weaker then equivalences (e.g. rewriting systems). The toolbox also extends the -automatic rewriting capabilities of the system, allowing to specify +automatic rewriting capabilities of the system, allowing the specification of custom strategies for rewriting. This documentation is adapted from the previous setoid documentation by diff --git a/plugins/extraction/README b/plugins/extraction/README index 64c871fd3..a9a7b04d5 100644 --- a/plugins/extraction/README +++ b/plugins/extraction/README @@ -6,7 +6,7 @@ What is it ? ------------ -The extraction is a mechanism allowing to produce functional code +The extraction is a mechanism that produces functional code (Ocaml/Haskell/Scheme) out of any Coq terms (either programs or proofs). diff --git a/plugins/romega/ReflOmegaCore.v b/plugins/romega/ReflOmegaCore.v index 7e4475d40..a1308e643 100644 --- a/plugins/romega/ReflOmegaCore.v +++ b/plugins/romega/ReflOmegaCore.v @@ -981,7 +981,7 @@ Inductive p_step : Set := | P_NOP : p_step. (* List of normalizations to perform : with a constructor of type - [p_step] allowing to visit both left and right branches, we would be + [p_step] allowing the visiting of both left and right branches, we would be able to restrict to only one normalization by hypothesis. And since all hypothesis are useful (otherwise they wouldn't be included), we would be able to replace [h_step] by a simple list. *) @@ -1014,7 +1014,7 @@ Inductive e_step : Set := (* For each reified data-type, we define an efficient equality test. It is not the one produced by [Decide Equality]. - Then we prove two theorem allowing to eliminate such equalities : + Then we prove two theorem allowing elimination of such equalities : \begin{verbatim} (t1,t2: typ) (eq_typ t1 t2) = true -> t1 = t2. (t1,t2: typ) (eq_typ t1 t2) = false -> ~ t1 = t2. diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v index 9e8f44c0f..fa33c1bf4 100644 --- a/theories/FSets/FMapAVL.v +++ b/theories/FSets/FMapAVL.v @@ -370,7 +370,7 @@ Fixpoint map_option (elt elt' : Type)(f : key -> elt -> option elt')(m : t elt) (** * Optimized map2 Suggestion by B. Gregoire: a [map2] function with specialized - arguments allowing to bypass some tree traversal. Instead of one + arguments that allows bypassing some tree traversal. Instead of one [f0] of type [key -> option elt -> option elt' -> option elt''], we ask here for: - [f] which is a specialisation of [f0] when first option isn't [None] diff --git a/theories/PArith/BinPosDef.v b/theories/PArith/BinPosDef.v index 4f8d9ee27..fcc12ab45 100644 --- a/theories/PArith/BinPosDef.v +++ b/theories/PArith/BinPosDef.v @@ -18,7 +18,7 @@ Require Export BinNums. -(** Postfix notation for positive numbers, allowing to mimic +(** Postfix notation for positive numbers, which allows mimicking the position of bits in a big-endian representation. For instance, we can write [1~1~0] instead of [(xO (xI xH))] for the number 6 (which is 110 in binary notation). @@ -557,4 +557,4 @@ Fixpoint of_succ_nat (n:nat) : positive := | S x => succ (of_succ_nat x) end. -End Pos.
\ No newline at end of file +End Pos. |