Merge PR #9774: Remove clutter by moving historic unmaintained dev/doc files to an archive subfolder.

Reviewed-by: ejgallego

8 files changed, 11 insertions, 14 deletions

diff --git a/dev/doc/COMPATIBILITY b/dev/doc/archive/COMPATIBILITY
index a81afca32d..a81afca32d 100644
--- a/dev/doc/COMPATIBILITY
+++ b/dev/doc/archive/COMPATIBILITY
diff --git a/dev/doc/extensions.txt b/dev/doc/archive/extensions.txt
index 075496db7c..36d63029f1 100644
--- a/dev/doc/extensions.txt
+++ b/dev/doc/archive/extensions.txt
@@ -16,4 +16,3 @@ Exemple de l'ajout de l'entrée "clause":
   faut rejouter clause dans le GLOBAL du GEXTEND
 
 - seulement après, le nom clause sera accessible dans les TACTIC EXTEND !
-
diff --git a/dev/doc/naming-conventions.tex b/dev/doc/archive/naming-conventions.tex
index 337b9226df..0b0811d81b 100644
--- a/dev/doc/naming-conventions.tex
+++ b/dev/doc/archive/naming-conventions.tex
@@ -133,7 +133,7 @@ has name \texttt{D\_integral}, then
 \end{quote}
 will have name \texttt{D\_integral\_inf}.
 
-As an exception, decidability statements, such as 
+As an exception, decidability statements, such as
 \begin{quote}
 \begin{tt}
 {forall x y, \{x = y\} + \{x <> y\}}
@@ -284,7 +284,7 @@ If the conclusion is in the other way than listed below, add suffix
 
 \itemrule{Nilpotency of element elt wrt a ring D with additive neutral
 element {\zero} and multiplicative binary operator
-{\op}}{Delt\_nilpotent} 
+{\op}}{Delt\_nilpotent}
 {op elt elt = zero}
 
   Remark: We leave the ring structure of D implicit; the general definition is ``exists n, iter n op elt = zero''.
@@ -487,7 +487,7 @@ binary relation {\rel}}{phi\_op\_rel, phi\_op\_rel\_morphism}
 {forall x y:D, phi (op x y) <-> rel (phi x) (phi y)}
 
 Remark: If the operator and the relation have similar name, one uses
-\texttt{phi\_op}. 
+\texttt{phi\_op}.
 
 Question: How to name each direction? (add \_elim for -> and \_intro
 for <- ?? -- as done in Bool.v ??)
diff --git a/dev/doc/newsyntax.tex b/dev/doc/archive/newsyntax.tex
index d1986fa0d1..71e964bcc9 100644
--- a/dev/doc/newsyntax.tex
+++ b/dev/doc/archive/newsyntax.tex
@@ -50,7 +50,7 @@
 La réflexion de la rénovation de la syntaxe des tactiques n'est pas
 encore aussi poussée que pour les termes (section~\ref{constrsyntax}),
 mais cette section vise à énoncer les quelques principes que l'on
-souhaite suivre. 
+souhaite suivre.
 
 \begin{itemize}
 \item Réutiliser les mots-clés de la syntaxe des termes (i.e. en
@@ -612,7 +612,7 @@ Fixpoint plus n m : nat {struct n} :=
 \subsection{Questions ouvertes}
 
 Voici les points sur lesquels la discussion est particulièrement
-ouverte: 
+ouverte:
 \begin{itemize}
 \item choix d'autres symboles pour les quantificateurs \TERM{!} et
   \TERM{?}. En l'état actuel des discussions, on garderait le \TERM{!}
diff --git a/dev/doc/notes-on-conversion.v b/dev/doc/archive/notes-on-conversion.v
index a81f170c63..a78ecd181a 100644
--- a/dev/doc/notes-on-conversion.v
+++ b/dev/doc/archive/notes-on-conversion.v
@@ -69,5 +69,3 @@ it is not convertible.
 The only hope to improve this problem is to observe that S' hides
 (behind two indirections) a Setoid constructor. This could be the
 argument to solve the problem.
-
-
diff --git a/dev/doc/old_svn_branches.txt b/dev/doc/archive/old_svn_branches.txt
index ee56ee24e9..ee56ee24e9 100644
--- a/dev/doc/old_svn_branches.txt
+++ b/dev/doc/archive/old_svn_branches.txt
diff --git a/dev/doc/perf-analysis b/dev/doc/archive/perf-analysis
index ac54fa6f73..ac54fa6f73 100644
--- a/dev/doc/perf-analysis
+++ b/dev/doc/archive/perf-analysis
diff --git a/dev/doc/versions-history.tex b/dev/doc/archive/versions-history.tex
index 1c4913d201..25dabad497 100644
--- a/dev/doc/versions-history.tex
+++ b/dev/doc/archive/versions-history.tex
@@ -135,7 +135,7 @@ Coq V5.8.3& released 6 December 1993 % Announce on coq-club
 
  & & 3 branches: Lyon (V5.8.x), Ulm (V5.10.x) and Rocq (V5.9)\\
 
-Coq V5.9 alpha& 7 July 1993 & 
+Coq V5.9 alpha& 7 July 1993 &
 experimental version based on evars refinement \\
               & & (merge from experimental ``V6.0'' and some pre-V5.8.3 \\
               & & version), not released\\
@@ -159,7 +159,7 @@ Coq V5.9 & 27 January 1993 & experimental version based on evars refinement\\
 \begin{tabular}{l|l|l}
 version & date & comments \\
 \hline
-Coq V5.10 ``Murthy'' & 22 January 1994 & 
+Coq V5.10 ``Murthy'' & 22 January 1994 &
 introduction of the ``DOPN'' structure\\
  & & \feature{eapply/prolog} tactics\\
  & & private use of cvs on madiran.inria.fr\\
@@ -179,7 +179,7 @@ Coq Lyon's archive & in 1994 & cvs server set up on woodstock.ens-lyon.fr\\
 
 Coq V5.10.9& announced on 17 August 1994 &
  % Announced by Catherine Parent on coqdev
- % Version avec une copie de THEORIES pour les inductifs mutuels 
+ % Version avec une copie de THEORIES pour les inductifs mutuels
  \\
 
 Coq V5.10.11& announced on 2 February 1995 & \feature{compute}\\
@@ -192,7 +192,7 @@ Coq V5.10.13& dated 9 June 1995 & on Lyon's cvs\\
 
 Coq V5.10.14.OO& dated 30 June 1995 & on Lyon's cvs\\
 
-Coq V5.10.14.a& announced 5 September 1995 & bug-fix release \\ % Announce on coq-club by BW 
+Coq V5.10.14.a& announced 5 September 1995 & bug-fix release \\ % Announce on coq-club by BW
 
 Coq V5.10.14.b& released 2 October 1995 & bug-fix release\\
   & & MS-DOS version released on 30 October 1995\\
@@ -203,7 +203,7 @@ Coq V5.10.14.b& released 2 October 1995 & bug-fix release\\
 
 Coq V5.10.15 & released 20 February 1996 & \feature{Logic, Sorting, new Sets and Relations libraries} \\
   % Announce on coq-club by BW
-  % dated 15 February 1996 and bound to pauillac's cvs in /net/pauillac/constr archive 
+  % dated 15 February 1996 and bound to pauillac's cvs in /net/pauillac/constr archive
   & & MacOS 7-9 version released on 1 March 1996 \\ % Announce on coq-club by BW
 
 Coq V5.11 & dated 1 March 1996 & not released, not in pauillac's CVS, \feature{eauto} \\
@@ -434,7 +434,7 @@ evars-based experimentation \\
  & & to Coq V5.7, version from October/November
 1992\\
 
-CtCoq & released 25 October 1995 & first beta-version  \\ % Announce on coq-club by Janet  
+CtCoq & released 25 October 1995 & first beta-version  \\ % Announce on coq-club by Janet
 
 Proto with explicit substitutions & 1997 &\\