diff options
| author | JPR | 2019-05-21 23:07:55 +0200 |
|---|---|---|
| committer | JPR | 2019-05-21 23:07:55 +0200 |
| commit | e6322e23958a937fa01960f8ce320717b9863253 (patch) | |
| tree | 79e2a8c8e7c953c44b3880fa683d82f2a6e6cc85 /dev/doc/archive | |
| parent | e9a5fe993ba36e22316ac9f6ef0564f38a3eb4f9 (diff) | |
Fixing typos - Part 1
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]\\ |