diff options
| author | Théo Zimmermann | 2019-05-22 17:38:06 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2019-05-22 17:38:06 +0200 |
| commit | 049cfe725d334fb863df31ee9e03db4b54a64455 (patch) | |
| tree | 2149121e604d2b369eb001289bf64adf508afc21 /dev/doc/archive | |
| parent | ed7d118e8ee9a6725daafde31845981f5da8d2b4 (diff) | |
| parent | 0001b6d108c2d2c058b0bfca7e0af888c026fe05 (diff) | |
Merge PR #10203: Fixing typos - Part 1
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Ack-by: cpitclaudel
Reviewed-by: gares
Reviewed-by: jfehrle
Reviewed-by: vbgl
Diffstat (limited to 'dev/doc/archive')
| -rw-r--r-- | dev/doc/archive/naming-conventions.tex | 6 | ||||
| -rw-r--r-- | dev/doc/archive/versions-history.tex | 2 |
2 files changed, 4 insertions, 4 deletions
diff --git a/dev/doc/archive/naming-conventions.tex b/dev/doc/archive/naming-conventions.tex index 0b0811d81b..8b0b14efb8 100644 --- a/dev/doc/archive/naming-conventions.tex +++ b/dev/doc/archive/naming-conventions.tex @@ -570,11 +570,11 @@ Example: \formula{eq\_true\_neg: \~{} eq\_true b <-> eq\_true (negb b)}. Zero on domain {\D} & D0 & (notation \verb=0=)\\ One on domain {\D} & D1 (if explicitly defined) & (notation \verb=1=)\\ Successor on domain {\D} & Dsucc\\ -Predessor on domain {\D} & Dpred\\ -Addition on domain {\D} & Dadd/Dplus\footnote{Coq historically uses \texttt{plus} and \texttt{mult} for addition and multiplication which are inconsistent notations, the recommendation is to use \texttt{add} and \texttt{mul} except in existng libraries that already use \texttt{plus} and \texttt{mult}} +Predecessor on domain {\D} & Dpred\\ +Addition on domain {\D} & Dadd/Dplus\footnote{Coq historically uses \texttt{plus} and \texttt{mult} for addition and multiplication which are inconsistent notations, the recommendation is to use \texttt{add} and \texttt{mul} except in existing libraries that already use \texttt{plus} and \texttt{mult}} & (infix notation \verb=+= [50,L])\\ Multiplication on domain {\D} & Dmul/Dmult\footnotemark[\value{footnote}] & (infix notation \verb=*= [40,L]))\\ -Soustraction on domain {\D} & Dminus & (infix notation \verb=-= [50,L])\\ +Subtraction on domain {\D} & Dminus & (infix notation \verb=-= [50,L])\\ Opposite on domain {\D} & Dopp (if any) & (prefix notation \verb=-= [35,R]))\\ Inverse on domain {\D} & Dinv (if any) & (prefix notation \verb=/= [35,R]))\\ Power on domain {\D} & Dpower & (infix notation \verb=^= [30,R])\\ diff --git a/dev/doc/archive/versions-history.tex b/dev/doc/archive/versions-history.tex index 25dabad497..46516dd4e4 100644 --- a/dev/doc/archive/versions-history.tex +++ b/dev/doc/archive/versions-history.tex @@ -372,7 +372,7 @@ Coq V8.4pl5& released 22 October 2014 & \\ Coq V8.4pl6& released 9 April 2015 & \\ Coq V8.5 beta1 & released 21 January 2015 & \feature{computation via compilation to OCaml} [22-1-2013]\\ -&& \feature{asynchonous evaluation} [8-8-2013]\\ +&& \feature{asynchronous evaluation} [8-8-2013]\\ && \feature{new proof engine deployed} [2-11-2013]\\ && \feature{universe polymorphism} [6-5-2014]\\ && \feature{primitive projections} [6-5-2014]\\ |