Mise à jour dev/doc/changes.txt et ajout d'un mot sur TACTIC EXTEND

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8857 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 76 insertions, 6 deletions

diff --git a/dev/README b/dev/README
index a4ca8f334a..0e40e82005 100644
--- a/dev/README
+++ b/dev/README
@@ -25,6 +25,8 @@ style.txt:     a few style recommendations for writing Coq ML files
 debugging.txt: help for debugging or profiling
 universes.txt: help to debug universes
 translate.txt: help to use coq translator
+extensions.txt: some help about TACTIC EXTEND
+
 header:        standard header for Coq ML files
 perf-analysis: analysis of perfs measured on the compilation of user contribs
 cic.dtd:       official dtd of the calc. of ind. constr. for im/ex-portation
diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index d1df2a810b..f60e3203f6 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -1,3 +1,49 @@
+=========================================
+= CHANGES BETWEEN COQ V8.0 AND COQ V8.1 =
+=========================================
+
+A few differences in Coq ML interfaces between Coq V8.0 and V8.1
+================================================================
+
+** Functions
+
+Util: option_app -> option_map
+Term: substl_decl -> subst_named_decl
+Lib: library_part -> remove_section_part
+Printer: prterm -> pr_lconstr
+Printer: prterm_env -> pr_lconstr_env
+Ppconstr: pr_sort -> pr_rawsort
+
+** Constructors
+
+Declarations: mind_consnrealargs -> mind_consnrealdecls
+NoRedun -> NoDup
+
+** Modules
+
+module Decl_kinds: new interface
+module Bigint: new interface
+module Tacred spawned module Redexpr
+module Symbols -> Notation
+module Coqast, Ast, Esyntax, Termast, and all other modules related to old
+  syntax are removed
+
+** Internal names
+
+OBJDEF and OBJDEF1 -> CANONICAL-STRUCTURE
+
+
+=========================================
+= CHANGES BETWEEN COQ V7.4 AND COQ V8.0 =
+=========================================
+
+See files in dev/syntax-v8
+
+
+==============================================
+= MAIN CHANGES BETWEEN COQ V7.3 AND COQ V7.4 =
+==============================================
+
 CHANGES DUE TO INTRODUCTION OF MODULES
 ======================================
 
@@ -183,8 +229,8 @@ Uses Declaremods to actually communicate with Global and to register
 objects.
 
 
-MAIN CHANGES FROM COQ V7.3
-==========================
+OTHER CHANGES
+=============
 
 Internal representation of tactics bindings has changed (see type
 Rawterm.substitution).
@@ -228,8 +274,10 @@ Tactics about False and not now in tactics/contradiction.ml
 Tactics depending on Init now tactics/*.ml4 (no longer in tactics/*.v)
 File tacinterp.ml moved from proofs to directory tactics
 
-MAIN CHANGES FROM COQ V7.1 TO COQ V7.2
-======================================
+
+==========================================
+= MAIN CHANGES FROM COQ V7.1 TO COQ V7.2 =
+==========================================
 
 The core of Coq (kernel) has meen minimized with the following effects:
 
@@ -242,8 +290,9 @@ the prefixes "Is" ans "IsMut" have been dropped from kind_of_term constructors,
 e.g. IsRel is now Rel, IsMutCase is now Case, etc.
 
 
-PRINCIPAUX CHANGEMENTS ENTRE COQ V6.3.1 ET COQ V7.0
-===================================================
+=======================================================
+= PRINCIPAUX CHANGEMENTS ENTRE COQ V6.3.1 ET COQ V7.0 =
+=======================================================
 
 Changements d'organisation / modules :
 --------------------------------------
diff --git a/dev/doc/extensions.txt b/dev/doc/extensions.txt
new file mode 100644
index 0000000000..eb4d265917
--- /dev/null
+++ b/dev/doc/extensions.txt
@@ -0,0 +1,19 @@
+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 !
+