Some documentation of recent changes concerning interfaces

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

3 files changed, 187 insertions, 0 deletions

diff --git a/CHANGES b/CHANGES
index 77701be7b..8408db0d9 100644
--- a/CHANGES
+++ b/CHANGES
@@ -23,6 +23,13 @@ Notations
 
 - "Bind Scope" can no longer bind "Funclass" and "Sortclass".
 
+Internal Infrastructure
+
+- Many reorganisations in the ocaml source files. For instance,
+  many internal a.s.t. of Coq are now placed in mli files in
+  a new directory intf/, for instance constrexpr.mli or glob_term.mli.
+  More details in dev/doc/changes.
+
 Changes from V8.4beta to V8.4beta2
 ==================================
 
diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index 322530e62..fd3c2e19a 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -1,4 +1,62 @@
 =========================================
+= CHANGES BETWEEN COQ V8.4 AND CQQ V8.5 =
+=========================================
+
+** Refactoring : more mli interfaces and simpler grammar.cma **
+
+- A new directory intf/ now contains mli-only interfaces :
+
+ Constrexpr : definition of constr_expr, was in Topconstr
+ Decl_kinds : now contains binding_kind = Explicit | Implicit
+ Evar_kinds : type Evar_kinds.t was previously Evd.hole_kind
+ Extend : was parsing/extend.mli
+ Genredexpr : regroup Glob_term.red_expr_gen and Tacexpr.glob_red_flag
+ Glob_term  : definition of glob_constr
+ Locus : definition of occurrences and stuff about clauses
+ Misctypes : intro_pattern_expr, glob_sort, cast_type, or_var, ...
+ Notation_term : contains notation_constr, was Topconstr.aconstr
+ Pattern : contains constr_pattern
+ Tacexpr : was tactics/tacexpr.ml
+ Vernacexpr : was toplevel/vernacexpr.ml
+
+- Many files have been divided :
+
+ vernacexpr: vernacexpr.mli + Locality
+ decl_kinds: decl_kinds.mli + Kindops
+ evd: evar_kinds.mli + evd
+ tacexpr: tacexpr.mli + tacops
+ glob_term: glob_term.mli + glob_ops + genredexpr.mli + redops
+ topconstr: constrexpr.mli + constrexpr_ops
+            + notation_expr.mli + notation_ops + topconstr
+ pattern: pattern.mli + patternops
+ libnames: libnames (qualid, reference) + globnames (global_reference)
+ egrammar: egramml + egramcoq
+
+- New utility files : miscops (cf. misctypes.mli) and
+  redops (cf genredexpr.mli).
+
+- Some other directory changes :
+  * grammar.cma and the source files specific to it are now in grammar/
+  * pretty-printing files are now in printing/
+
+- Inner-file changes :
+
+  * aconstr is now notation_constr, all constructors for this type
+    now start with a N instead of a A (e.g. NApp instead of AApp),
+    and functions about aconstr may have been renamed (e.g. match_aconstr
+    is now match_notation_constr).
+
+  * occurrences (now in Locus.mli) is now an algebraic type, with
+    - AllOccurrences instead of all_occurrences_expr = (false,[])
+    - (AllOccurrencesBut l) instead of (all_occurrences_expr_but l) = (false,l)
+    - NoOccurrences instead of no_occurrences_expr = (true,[])
+    - (OnlyOccurrences l) instead of (no_occurrences_expr_but l) = (true,l)
+
+  * move_location (now in Misctypes) has two new constructors
+    MoveFirst and MoveLast replacing (MoveToEnd false) and (MoveToEnd true)
+
+
+=========================================
 = CHANGES BETWEEN COQ V8.3 AND COQ V8.4 =
 =========================================
 
diff --git a/dev/doc/coq-src-description.txt b/dev/doc/coq-src-description.txt
new file mode 100644
index 000000000..fe896d316
--- /dev/null
+++ b/dev/doc/coq-src-description.txt
@@ -0,0 +1,122 @@
+
+Coq main source components (in link order)
+------------------------------------------
+
+clib : Basic files in lib/, such as util.ml
+lib : Other files in lib/
+kernel
+library
+pretyping
+interp
+proofs
+printing
+parsing
+tactics
+toplevel
+
+highparsing :
+
+ Files in parsing/ that cannot be linked too early.
+ Contains the grammar rules g_*.ml4
+
+hightactics :
+
+ Files in tactics/ that cannot be linked too early.
+ These are the .ml4 files that uses the EXTEND possibilities
+ provided by grammar.cma, for instance eauto.ml4.
+
+
+Special components
+------------------
+
+intf :
+
+ Contains mli-only interfaces, many of them providing a.s.t.
+ used for dialog bewteen coq components. Ex: Constrexpr.constr_expr
+ produced by parsing and transformed by interp.
+
+grammar :
+
+ Camlp4 syntax extensions. The file grammar/grammar.cma is used
+ to pre-process .ml4 files containing EXTEND constructions,
+ either TACTIC EXTEND, ARGUMENTS EXTEND or VERNAC ... EXTEND.
+ This grammar.cma incorporates many files from other directories
+ (mainly parsing/), plus some specific files in grammar/.
+ The other syntax extension grammar/q_constr.cmo is a addition to
+ grammar.cma with a constr PATTERN quotation.
+
+
+Hierarchy of A.S.T.
+-------------------
+
+*** Terms ***
+
+             ...          ...
+              |            /\
+    parsing   |            | printing
+              |            |
+              V            |
+           Constrexpr.constr_expr
+              |            /\
+ constrintern |            | constrextern
+  (in interp) |            | (in interp)
+globalization |            |
+              V            |
+           Glob_term.glob_constr
+              |            /\
+    pretyping |            | detyping
+              |            | (in pretyping)
+              V            |
+               Term.constr
+                 |     /\
+   safe_typing   |      |
+   (validation   |      |
+    by kernel)   |______|
+
+
+*** Patterns ***
+
+  |
+  | parsing
+  V
+constr_pattern_expr = constr_expr
+  |
+  | Constrintern.interp_constr_pattern (in interp)
+  | reverse way in Constrextern
+  V
+Pattern.constr_pattern
+  |
+  ---> used for instance by Matching.matches (in pretyping)
+
+
+*** Notations ***
+
+
+Notation_term.notation_constr
+
+Conversion from/to glob_constr in Notation_ops
+
+TODO...
+
+
+*** Tactics ***
+
+ |
+ | parsing
+ V
+Tacexpr.raw_tactic_expr
+ |
+ | Tacinterp.intern_pure_tactic (?)
+ V
+Tacexpr.glob_tactic_expr
+ |
+ | Tacinterp.eval_tactic (?)
+ V
+Proof_type.tactic
+
+TODO: check with Hugo
+
+
+*** Vernac expressions ***
+
+Vernacexpr.vernac_expr, produced by parsing, used in Vernacentries and Vernac