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

Reviewed-by: ejgallego

1 files changed, 18 insertions, 0 deletions

diff --git a/dev/doc/archive/extensions.txt b/dev/doc/archive/extensions.txt
new file mode 100644
index 0000000000..36d63029f1
--- /dev/null
+++ b/dev/doc/archive/extensions.txt
@@ -0,0 +1,18 @@
+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 !