Remove clutter by moving historic unmaintained dev/doc files to an archive subfolder.

1 files changed, 0 insertions, 19 deletions

diff --git a/dev/doc/extensions.txt b/dev/doc/extensions.txt
deleted file mode 100644
index 075496db7c..0000000000
--- a/dev/doc/extensions.txt
+++ /dev/null
@@ -1,19 +0,0 @@
-Comment ajouter une nouvelle entrée primitive pour les TACTIC EXTEND ?
-======================================================================
-
-Exemple de l'ajout de l'entrée "clause":
-
-- ajouter un type ClauseArgType dans interp/genarg.ml{,i}, avec les
-  wit_, rawwit_, et globwit_ correspondants
-
-- ajouter partout où Genarg.argument_type est filtré le cas traitant de
-  ce nouveau ClauseArgType
-
-- utiliser le rawwit_clause pour définir une entrée clause du bon
-  type et du bon nom dans le module Tactic de pcoq.ml4
-
-- il faut aussi exporter la règle hors de g_tactic.ml4. Pour cela, il
-  faut rejouter clause dans le GLOBAL du GEXTEND
-
-- seulement après, le nom clause sera accessible dans les TACTIC EXTEND !
-