15 files changed, 792 insertions, 514 deletions
diff --git a/dev/doc/build-system.dev.txt b/dev/doc/build-system.dev.txt
index 3d9cba14..af1120e9 100644
--- a/dev/doc/build-system.dev.txt
+++ b/dev/doc/build-system.dev.txt
@@ -1,21 +1,38 @@
 
-Since July 2007, Coq features a build system overhauled by Pierre
-Corbineau and Lionel Elie Mamane.
-
----------------------------------------------------------------------
-WARNING:
-In March 2010 this build system has been heavily adapted by Pierre
-Letouzey. In particular there no more explicit stage1,2. Stage3
-was removed some time ago when coqdep was splitted into coqdep_boot
-and full coqdep. Ideas are still similar to what is describe below,
-but:
-1) .ml4 are explicitely turned into .ml files, which stay after build
-2) we let "make" handle the inclusion of .d without trying to guess
-   what could be done at what time. Some initial inclusions hence
-  _fail_, but "make" tries again later and succeed.
-
-TODO: remove obsolete sections below and better describe the new approach
------------------------------------------------------------------------
+
+HISTORY:
+-------
+
+* July 2007 (Pierre Corbineau & Lionel Elie Mamane).
+  Inclusion of a build system with 3 explicit phases:
+  - Makefile.stage1: ocamldep, sed, camlp4 without Coq grammar extension
+  - Makefile.stage2: camlp4 with grammar.cma or q_constr.cmo
+  - Makefile.stage3: coqdep (.vo)
+
+* March 2010 (Pierre Letouzey).
+  Revised build system. In particular, no more stage1,2,3 :
+  - Stage3 was removed some time ago when coqdep was splitted into
+    coqdep_boot and full coqdep.
+  - Stage1,2 were replaced by brutal inclusion of all .d at the start
+    of Makefile.build, without trying to guess what could be done at
+    what time. Some initial inclusions hence _fail_, but "make" tries
+    again later and succeed.
+  - Btw, .ml4 are explicitely turned into .ml files, which stay after build.
+    By default, they are in binary ast format, see READABLE_ML4 option.
+
+* February 2014 (Pierre Letouzey).
+  Another revision of the build system. We avoid relying on the awkward
+  include-which-fails-but-works-finally-after-a-retry feature of gnu make.
+  This was working, but was quite hard to understand. Instead, we reuse
+  the idea of two explicit phases, but in a lighter way than in 2007.
+  The main Makefile calls Makefile.build twice :
+  - first for building grammar.cma (and q_constr.cmo), with a
+    restricted set of .ml4 (see variable BUILDGRAMMAR).
+  - then on the true target asked by the user.
+
+    
+---------------------------------------------------------------------------
+
 
 This file documents internals of the implementation of the build
 system. For what a Coq developer needs to know about the build system,
@@ -24,68 +41,47 @@ see build-system.txt .
 .ml4 files
 ----------
 
-.ml files corresponding to .ml4 files are created to keep ocamldep
-happy only. To ensure they are not used for compilation, they contain
-invalid OCaml.
-
+.ml4 are converted to .ml by camlp4. By default, they are produced
+in the binary ast format understood by ocamlc/ocamlopt/ocamldep.
+Pros:
+ - faster than parsing clear-text source file.
+ - no risk of editing them by mistake instead of the .ml4
+ - the location in the binary .ml are those of the initial .ml4,
+   hence errors are properly reported in the .ml4.
+Cons:
+ - This format may depend on your ocaml version, they should be
+   cleaned if you change your build environment.
+ - Unreadable in case you want to inspect this generated code.
+   For that, use make with the READABLE_ML4=1 option to switch to
+   clear-text generated .ml.
 
-multi-stage build
------------------
 
-Le processus de construction est séparé en trois étapes qui correspondent
-aux outils nécessaires pour calculer les dépendances de cette étape:
-
-stage1: ocamldep, sed , camlp4 sans fichiers de Coq
-stage2: camlp4 avec grammar.cma et/ou q_constr.cmo
-stage3: coqdep (.vo)
+Makefiles hierachy
+------------------
 
 Le Makefile a été séparé en plusieurs fichiers :
 
-- Makefile: coquille vide qui délègue les cibles à la bonne étape sauf
-  clean et les fichiers pour emacs (car ils sont en quelque sorte en
-  "stage0": aucun calcul de dépendance nécessaire).
+- Makefile: coquille vide qui lançant Makefile.build sauf pour
+  clean et quelques petites choses ne nécessitant par de calculs
+  de dépendances.
 - Makefile.common : définitions des variables (essentiellement des
   listes de fichiers)
-- Makefile.build : les règles de compilation sans inclure de
-  dépendances
-- Makefile.stage* : fichiers qui incluent les dépendances calculables
-  à cette étape ainsi que Makefile.build.
-
-The build needs to be cut in stages because make will not take into
-account one include when making another include.
+- Makefile.build : contient les regles de compilation, ainsi que
+  le "include" des dépendances (restreintes ou non selon la variable
+  BUILDGRAMMAR).
+- Makefile.doc : regles specifiques à la compilation de la documentation.
 
 
 Parallélisation
 ---------------
 
-Le découpage en étapes veut dire que le makefile est un petit peu
-moins parallélisable que strictement possible en théorie: par exemple,
-certaines choses faites en stage2 pourraient être faites en parallèle
-avec des choses de stage1. Nous essayons de minimiser cet effet, mais
-nous ne l'avons pas complètement éliminé parce que cela mènerait à un
-makefile très complexe. La minimisation est principalement que si on
-demande un objet spécifique (par exemple "make parsing/g_constr.cmx"),
-il est fait dans l'étape la plus basse possible (simplement), mais si
-un objet est fait comme dépendance de la cible demandée (par exemple
-dans un "make world"), il est fait le plus tard possible (par exemple,
-tout code OCaml non nécessaire pour coqdep ni grammar.cma ni
-q_constr.cmo est compilé en stage3 lors d'un "make world"; cela permet
-le parallélisme de compilation de code OCaml et de fichiers Coq (.v)).
-
-Le "(simplement)" ci-dessus veut dire que savoir si un fichier non
-nécessaire pour grammar.cma/q_constr.cmo peut en fait être fait en
-stage1 est compliqué avec make, alors nous retombons en général sur le
-stage2. La séparation entre le stage2 et stage3 est plus facile, donc
-l'optimisation ci-dessus s'y applique pleinement.
-
-En d'autres mots, nous avons au niveau conceptuel deux assignations
-d'étape pour chaque fichier:
-
- - l'étape la plus petite où nous savons qu'il peut être fait.
- - l'étape la plus grande où il peut être fait.
-
-Mais seule la première est gérée explicitement, la seconde est
-implicite.
+Il y a actuellement un double appel interne à "make -f Makefile.build",
+d'abord pour construire grammar.cma/q_constr.cmo, puis le reste.
+Cela signifie que ce makefile est un petit peu moins parallélisable
+que strictement possible en théorie: par exemple, certaines choses
+faites lors du second make pourraient être faites en parallèle avec
+le premier. En pratique, ce premier make va suffisemment vite pour
+que cette limitation soit peu gênante.
 
 
 FIND_VCS_CLAUSE
diff --git a/dev/doc/build-system.txt b/dev/doc/build-system.txt
index b243ebe2..31d9875a 100644
--- a/dev/doc/build-system.txt
+++ b/dev/doc/build-system.txt
@@ -1,26 +1,8 @@
-Since July 2007, Coq features a build system overhauled by Pierre
-Corbineau and Lionel Elie Mamane.
-
----------------------------------------------------------------------
-WARNING:
-In March 2010 this build system has been heavily adapted by Pierre
-Letouzey. In particular there no more explicit stage1,2. Stage3
-was removed some time ago when coqdep was splitted into coqdep_boot
-and full coqdep. Ideas are still similar to what is describe below,
-but:
-1) .ml4 are explicitely turned into .ml files, which stay after build
-2) we let "make" handle the inclusion of .d without trying to guess
-   what could be done at what time. Some initial inclusions hence
-  _fail_, but "make" tries again later and succeed.
-
-TODO: remove obsolete sections below and better describe the new approach
------------------------------------------------------------------------
 
 This file documents what a Coq developer needs to know about the build
 system. If you want to enhance the build system itself (or are curious
-about its implementation details), see build-system.dev.txt .
-
-The build system is not at its optimal state, see TODO section.
+about its implementation details), see build-system.dev.txt, and in
+particular its initial HISTORY section.
 
 
 FAQ: special features used in this Makefile
@@ -51,22 +33,10 @@ $(subst ...), $(patsubst ...), $(shell ...), $(foreach ...), $(if ...)
 * Behavior of -include
 
 If the file given to -include doesn't exist, make tries to build it,
-but doesn't care if this build fails. This can be quite surprising,
-see in particular the -include in Makefile.stage*
-
-
-Stages in build system
-----------------------
-
-The build system is separated into three stages, corresponding to the
-tool(s) necessary to compute the dependencies necessary at this stage:
-
-stage1: ocamldep, sed, camlp4 without Coq extensions
-stage2: camlp4 with grammar.cma and/or q_constr.cmo
-stage3: coqdep (.vo)
-
-The file "Makefile" itself serves as minimum stage for targets that
-should not need any dependency (such as *clean*).
+and even retries again if necessary, but doesn't care if this build
+finally fails. We used to rely on this "feature", but this should not
+be the case anymore. We kept "-include" instead of "include" for
+avoiding warnings about initially non-existant files.
 
 Changes (for old-timers)
 ------------------------
@@ -97,40 +67,11 @@ save precious time:
 
  - Always ask for what you want directly (e.g. bin/coqtop,
    foo/bar.cmo, ...), don't do "make world" and interrupt
-   it when it has done what you want. This will try to minimise the
-   stage at which what you ask for is done (instead of maximising it
-   in order to maximise parallelism of the build process).
-
+   it when it has done what you want.
    For example, if you only want to test whether bin/coqtop still
    builds (and eventually start it to test your bugfix or new
-   feature), don't do "make world" and interrupt it when bin/coqtop is
-   built. Use "make bin/coqtop" or "make coqbinaries" or something
-   like that. This will avoid entering the stage 3, and cut build
-   system overhead by 50% (1.2s instead of 2.4 on writer's machine).
-
- - You can turn off rebuilding of the standard library each time
-   bin/coqtop is rebuilt with NO_RECOMPILE_LIB=1.
-
- - If you want to avoid all .ml4 files being recompiled only because
-   grammar.cma was rebuilt, do "make ml4depclean" once and then use
-   NO_RECOMPILE_ML4=1.
-
- - The CM_STAGE1=1 option to make will build all .cm* files mentioned
-   as targets on the command line in stage1. Whether this will work is
-   your responsibility. It should work for .ml files that don't depend
-   (nor directly nor indirectly through transitive closure of the
-   dependencies) on any .ml4 file, or where those dependencies can be
-   safely ignored in the current situation (e.g. all these .ml4 files
-   don't need to be recompiled).
-
-   This will avoid entering the stage2 (a reduction of 33% in
-   overhead, 0.4s on the writer's machine).
-
- - To jump directly into a stage (e.g. because you know nothing is to
-   be done in stage 1 or (1 and 2) or because you know that the target
-   you give can be, in this situation, done in a lower stage than the
-   build system dares to), use GOTO_STAGE=n. This will jump into stage
-   n and try to do the targets you gave in that stage.
+   feature), use "make bin/coqtop" or "make coqbinaries" or something
+   like that.
 
  - To disable all dependency recalculation, use the NO_RECALC_DEPS=1
    option. It disables REcalculation of dependencies, not calculation
@@ -138,12 +79,6 @@ save precious time:
    still created, but it is not updated every time the source file
    (e.g. .ml) is changed.
 
-General speed improvements:
-
- - When building both the native and bytecode versions, the
-   KEEP_ML4_PREPROCESSED=1 option may reduce global compilation time
-   by running camlp4o only once on every .ml4 file, at the expense of
-   readability of compilation error messages for .ml4 files.
 
 Dependencies
 ------------
@@ -181,166 +116,30 @@ Targets for cleaning various parts:
 .ml4 files
 ----------
 
-The camlp4-preprocessed version of FOO.ml4 is FOO.ml4-preprocessed and
-can be obtained with:
- make FOO.ml4-preprocessed
-
 If a .ml4 file uses a grammar extension from Coq (such as grammar.cma
 or q_constr.cmo), it must contain a line like:
  (*i camlp4deps: "grammar.cma q_constr.cmo" i*)
 
-If it uses a standard grammar extension, it must contain a line like:
- (*i camlp4use: "pa_ifdef.cmo" i*)
-
-It can naturally contain both a camlp4deps and a camlp4use line. Both
-are used for preprocessing. It is thus _not_ necessary to add a
-specific rule for a .ml4 file in the Makefile.build just because it
-uses grammar extensions.
-
-By default, the build system is geared towards development that may
-use the Coq grammar extensions, but not development of Coq's grammar
-extensions themselves. This means that .ml4 files are compiled
-directly (using ocamlc/opt's -pp option), without use of an
-intermediary .ml (or .ml4-preprocessed) file. This is so that if a
-compilation error occurs, the location in the error message is a
-location in the .ml4 file. If you are modifying the grammar
-extensions, you may be more interested in the location of the error in
-the .ml4-preprocessed file, so that you can see what your new grammar
-extension made wrong. In that case, use the KEEP_ML4_PREPROCESSED=1
-option. This will make compilation of a .ml4 file a two-stage process:
-
-1) create the .ml4-preprocessed file with camlp4o
-2) compile it with straight ocamlc/opt without preprocessor
-
-and will instruct make not to delete .ml4-preprocessed files
-automatically just because they are intermediary files, so that you
-can inspect them.
-
-If you add a _new_ grammar extension to Coq:
-
- - if it can be built at stage1, that is the .ml4 file does not use a
-   Coq grammar extension itself, then add it, and all .cmo files it
-   needs to STAGE1_TARGETS and STAGE_ML4 in Makefile.common. See the
-   handling of grammar.cma and q_constr.cmo for an example.
-
- - if it cannot be built at stage1, that is the .ml4 file itself needs
-   to be preprocessed with a Coq camlp4 grammar extension, then,
-   congratulations, you need to add a new stage between stage1 and
-   stage2.
+The use of (*i camlp4use: ... i*) to mention uses of standard
+extension such as IFDEF has been discontinued, the Makefile now
+always calls camlp4 with pa_macros.cmo and a few others by default.
+
+For debugging a Coq grammar extension, it could be interesting
+to use the READABLE_ML4=1 option, otherwise the generated .ml are
+in an internal binary format (see build-system.dev.txt).
+
 
 New files
 ---------
 
 For a new file, in most cases, you just have to add it to the proper
-file list(s) in Makefile.common, such as ARITHVO or TACTICS.
+file list(s):
+ - For .ml, in the corresponding .mllib (e.g. kernel/kernel.mllib)
+   These files are also used by the experimental ocamlbuild plugin,
+   which is quite touchy about them : be careful with order,
+   duplicated entries, whitespace errors, and do not mention .mli there.
+ - For .v, in the corresponding vo.itarget (e.g theories/Init/vo.itarget)
+ - The definitions in Makefile.common might have to be adapted too.
+ - If your file needs a specific rule, add it to Makefile.build
 
 The list of all ml4 files is not handled manually anymore.
-
-Exceptions are:
-
- - The file is necessary at stage1, that it is necessary to build the
-   Coq camlp4 grammar extensions. In this case, make sure it ends up
-   in STAGE1_CMO and (for .ml4 files) STAGE1_ML4. See the handling of
-   grammar.cma and/or q_constr.cmo for an example.
-
- - if the file needs to be compiled with -rectypes, add it to
-   RECTYPESML in Makefile.common. If it is a .ml4 file, implement
-   RECTYPESML4 or '(*i ocamlflags i*)'; see TODO.
-
- - the file needs a specific Makefile entry; add it to Makefile.build
-
- - the files produced from the added file do not match an existing
-   pattern or entry in "Makefile". (All the common cases of
-   .ml{,i,l,y,4}, .v, .c, ... files that produces (respectively)
-   .cm[iox], .vo, .glob, .o, ... files with the same basename are
-   already covered.) In this case, see section "New targets".
-
-New targets
------------
-
-If you want to add:
-
- - a new PHONY target to the build system, that is a target that is
-   not the name of the file it creates,
-
- - a normal target is not already mapped to a stage by "Makefile"
-
- then:
-
- - add the necessary rule to Makefile.build, if any
- - add the target to STAGEn_TARGETS, with n being the smallest stage
-   it can be built at, that is:
-   * 1 for OCaml code that doesn't use any Coq camlp4 grammar extension
-   * 2 for OCaml code that uses (directly or indirectly) a Coq
-       camlp4 grammar extension. Indirectly means a dependency of it
-       does.
-   * 3 for Coq (.v) code.
-
-   *or*
-
-   add a pattern matching the target to the pattern lists for the
-   smallest stage it can be built at in "Makefile".
-
-TODO
-----
-
-delegate pa_extend.cmo to camlp4use statements and remove it from
-standard camlp4 options.
-
-maybe manage compilation flags (such as -rectypes or the CoqIDE ones)
-from a
- (*i ocamlflags: "-rectypes" i*)
-statement in the .ml(4) files themselves, like camlp4use. The CoqIDE
-files could have
- (*i ocamlflags: "${COQIDEFLAGS}" i*)
-and COQIDEFLAGS is still defined (and exported by) the Makefile.build.
-
-Clean up doc/Makefile
-
-config/Makefile looks like it contains a lot of unused variables,
-clean that up (are any maybe used by nightly scripts on
-pauillac?). Also, the COQTOP variable from config/Makefile (and used
-in contribs) has a very poorly chosen name, because "coqtop" is the
-name of a Coq executable! In the coq Makefiles, $(COQTOPEXE) is used
-to refer to that executable.
-
-Promote the granular .glob handling to official way of doing things
-for Coq developments, that is implement it in coq_makefile and the
-contribs. Here are a few hints:
-
->> Les fichiers de constantes produits par -dump-glob sont maintenant
->> produits par fichier et sont ensuite concaténés dans
->> glob.dump. Ilsont produits par défaut (avec les bonnes
->> dépendances).
-
-> C'est une chose que l'on voulait faire aussi.
-
-(J'ai testé et débogué ce concept sur CoRN dans les derniers mois.)
-
-> Est-ce que vous sauriez modifier coq_makefile pour qu'il procède de
-> la même façon
-
-Dans cette optique, il serait alors plus propre de changer coqdep pour
-qu'il produise directement l'output que nous mettons maintenant dans
-les .v.d (qui est celui de coqdoc post-processé avec sed).
-
-Si cette manière de gérer les glob devient le standard béni
-officiellement par "the Coq development team", ne voudrions nous pas
-changer coqc pour qu'il produise FOO.glob lors de la compilation de
-FOO.v par défaut (sans argument "-dump-glob")?
-
-> et que la production de a.html par coqdoc n'ait une dépendance qu'en
-> les a.v et a.glob correspondant ?
-
-Je crois que coqdoc exige un glob-dump unique, il convient donc de
-concaténer les .glob correspondants. Soit un glob-dump global par
-projet (par Makefile), soit un glob-dump global par .v(o), qui
-contient son .glob et ceux de tous les .v(o) atteignables par le
-graphe des dépendances. CoRN contient déjà un outil de calcul de
-partie atteignable du graphe des dépendances (il y est pour un autre
-usage, pour calculer les .v à mettre dans les différents tarballs sur
-http://corn.cs.ru.nl/download.html; les parties partielles sont
-définies par liste de fichiers .v + toutes leurs dépendances
-(in)directes), il serait alors adéquat de le mettre dans les tools de
-Coq.
-
diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index 322530e6..2f62be9a 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -1,4 +1,103 @@
 =========================================
+= 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)
+
+- API of pretyping.ml and constrintern.ml has been made more uniform
+  * Parametrization of understand_* functions is now made using
+    "inference flags"
+  * Functions removed:
+    - interp_constr_judgment (inline its former body if really needed)
+    - interp_casted_constr, interp_type: use instead interp_constr with
+      expected_type set to OfType or to IsType
+    - interp_gen: use any of interp_constr, interp_casted_constr, interp_type
+    - interp_open_constr_patvar
+    - interp_context: use interp_context_evars (with a "evar_map ref") and
+      call solve_remaining_evars afterwards with a failing flag
+      (e.g. all_and_fail_flags)
+    - understand_type, understand_gen: use understand with appropriate
+      parameters
+  * Change of semantics:
+    - Functions interp_*_evars_impls have a different interface and do
+      not any longer check resolution of evars by default; use
+      check_evars_are_solved explicitly to check that evars are solved.
+  See also the corresponding commit log.
+
+- Tactics API: new_induct -> induction; new_destruct -> destruct;
+  letin_pat_tac do not accept a type anymore
+
+- New file find_subterm.ml for gathering former functions
+  subst_closed_term_occ_modulo, subst_closed_term_occ_decl (which now
+  take and outputs also an evar_map), and
+  subst_closed_term_occ_modulo, subst_closed_term_occ_decl_modulo (now
+  renamed into replace_term_occ_modulo and
+  replace_term_occ_decl_modulo).
+
+- API of Inductiveops made more uniform (see commit log or file itself).
+
+- API of intros_pattern style tactic changed; "s" is dropped in
+  "intros_pattern" and "intros_patterns" is not anymore behaving like
+  tactic "intros" on the empty list.
+
+- API of cut tactics changed: for instance, cut_intro should be replaced by
+  "assert_after Anonymous"
+
+- All functions taking an env and a sigma (or an evdref) now takes the
+  env first.
+
+=========================================
 = CHANGES BETWEEN COQ V8.3 AND COQ V8.4 =
 =========================================
 
@@ -516,14 +615,14 @@ Changements d'organisation / modules :
   Std, More_util		-> lib/util.ml
 
   Names				-> kernel/names.ml et kernel/sign.ml
-    (les parties noms et signatures ont �t� s�par�es)
+    (les parties noms et signatures ont été séparées)
 
-  Avm,Mavm,Fmavm,Mhm  ->  utiliser plut�t Map (et freeze alors gratuit)
+  Avm,Mavm,Fmavm,Mhm  ->  utiliser plutôt Map (et freeze alors gratuit)
   Mhb                 ->  Bij
 
-  Generic est int�gr� � Term (et un petit peu � Closure)
+  Generic est intégré à Term (et un petit peu à Closure)
 
-Changements dans les types de donn�es :
+Changements dans les types de données :
 ---------------------------------------
   dans Generic: free_rels : constr -> int Listset.t
                   devient : constr -> Intset.t
@@ -543,7 +642,7 @@ ATTENTION:
   
 		try . .. with UserError _ -> ...
 
-  mais �crire � la place
+  mais écrire à la place
  
                 try ... with e when Logic.catchable_exception e -> ...
 
@@ -675,7 +774,7 @@ Changements dans les inductifs
 Nouveaux types "constructor" et "inductive" dans Term
 La plupart des fonctions de typage des inductives prennent maintenant
 un inductive au lieu d'un oonstr comme argument. Les seules fonctions
-� traduire un constr en inductive sont les find_rectype and co.
+à traduire un constr en inductive sont les find_rectype and co.
 
 Changements dans les grammaires
 -------------------------------
@@ -683,9 +782,9 @@ Changements dans les grammaires
  . le lexer (parsing/lexer.mll) est maintenant un lexer ocamllex
 
  . attention : LIDENT -> IDENT  (les identificateurs n'ont pas de
-                                 casse particuli�re dans Coq)
+                                 casse particulière dans Coq)
 
- . Le mot "command" est remplac� par "constr" dans les noms de
+ . Le mot "command" est remplacé par "constr" dans les noms de
  fichiers, noms de modules et non-terminaux relatifs au parsing des
  termes; aussi les changements suivants "COMMAND"/"CONSTR" dans
  g_vernac.ml4, VARG_COMMAND/VARG_CONSTR dans vernac*.ml*
@@ -693,22 +792,22 @@ Changements dans les grammaires
  . Les constructeurs d'arguments de tactiques IDENTIFIER, CONSTR, ...n
    passent en minuscule Identifier, Constr, ...
  
- . Plusieurs parsers ont chang� de format (ex: sortarg)
+ . Plusieurs parsers ont changé de format (ex: sortarg)
 
 Changements dans le pretty-printing
 -----------------------------------
 
- . D�couplage de la traduction de constr -> rawconstr (dans detyping)
+ . Découplage de la traduction de constr -> rawconstr (dans detyping)
     et de rawconstr -> ast (dans termast)
- . D�placement des options d'affichage de printer vers termast
- . D�placement des r�aiguillage d'univers du pp de printer vers esyntax
+ . Déplacement des options d'affichage de printer vers termast
+ . Déplacement des réaiguillage d'univers du pp de printer vers esyntax
 
 	
 Changements divers
 ------------------
 
  . il n'y a plus de script coqtop => coqtop et coqtop.byte sont
-   directement le r�sultat du link du code
+   directement le résultat du link du code
    => debuggage et profiling directs
 
  . il n'y a plus d'installation locale dans bin/$ARCH
diff --git a/dev/doc/coq-src-description.txt b/dev/doc/coq-src-description.txt
new file mode 100644
index 00000000..fe896d31
--- /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
diff --git a/dev/doc/debugging.txt b/dev/doc/debugging.txt
index 2480b8ed..f0df2fc3 100644
--- a/dev/doc/debugging.txt
+++ b/dev/doc/debugging.txt
@@ -21,14 +21,6 @@ Debugging from Coq toplevel using Caml trace mechanism
   notations, ...), use "Set Printing All". It will affect the #trace
   printers too.
 
-Note for Ocaml 3.10.x: Ocaml 3.10.x requires that modules compiled
-with -rectypes are loaded in an environment with -rectypes set but
-there is no way to tell the toplevel to support -rectypes. To make it
-works, use "patch -p0 < dev/doc/patch.ocaml-3.10.drop.rectypes" to
-hack script/coqmktop.ml, then recompile coqtop.byte. The procedure
-above then works as soon as coqtop.byte is called with at least one
-argument (add neutral option -byte to ensure at least one argument).
-
 
 Debugging from Caml debugger
 ============================
diff --git a/dev/doc/extensions.txt b/dev/doc/extensions.txt
index eb4d2659..075496db 100644
--- a/dev/doc/extensions.txt
+++ b/dev/doc/extensions.txt
@@ -1,19 +1,19 @@
-Comment ajouter une nouvelle entr�e primitive pour les TACTIC EXTEND ?
+Comment ajouter une nouvelle entrée primitive pour les TACTIC EXTEND ?
 ======================================================================
 
-Exemple de l'ajout de l'entr�e "clause":
+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
+- 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
+- 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
+- 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 !
+- seulement après, le nom clause sera accessible dans les TACTIC EXTEND !
 
diff --git a/dev/doc/naming-conventions.tex b/dev/doc/naming-conventions.tex
index e7c8975b..34916494 100644
--- a/dev/doc/naming-conventions.tex
+++ b/dev/doc/naming-conventions.tex
@@ -1,6 +1,6 @@
 \documentclass[a4paper]{article}
 \usepackage{fullpage}
-\usepackage[latin1]{inputenc}
+\usepackage[utf8]{inputenc}
 \usepackage[T1]{fontenc}
 \usepackage{amsfonts}
 
@@ -299,7 +299,7 @@ element {\zero} and multiplicative binary operator
     (for \texttt{Z}, \texttt{Q} and \texttt{R}), \texttt{eq\_mul\_0} (for
     \texttt{NZ}).
 
-  Remark: The French school says ``integrit�''.
+  Remark: The French school says ``integrité''.
 
 \itemrule{Nilpotency of binary operator {\op} wrt to its absorbing element
 zero in D}{Dop\_nilpotent} {forall x, op x x = zero}
diff --git a/dev/doc/newsyntax.tex b/dev/doc/newsyntax.tex
index 96e61292..d1986fa0 100644
--- a/dev/doc/newsyntax.tex
+++ b/dev/doc/newsyntax.tex
@@ -5,7 +5,7 @@
 
 \usepackage{verbatim}
 \usepackage[T1]{fontenc}
-\usepackage[latin1]{inputenc}
+\usepackage[utf8]{inputenc}
 \usepackage[french]{babel}
 \usepackage{amsmath}
 \usepackage{amssymb}
@@ -15,7 +15,7 @@
 \author{B.~Barras}
 \title{Proposition de syntaxe pour Coq}
 
-%% Le _ est un caract�re normal
+%% Le _ est un caractère normal
 \catcode`\_=13
 \let\subscr=_
 \def_{\ifmmode\sb\else\subscr\fi}
@@ -47,21 +47,21 @@
 \section{Grammaire des tactiques}
 \label{tacticsyntax}
 
-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
+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. 
 
 \begin{itemize}
-\item R�utiliser les mots-cl�s de la syntaxe des termes (i.e. en
+\item Réutiliser les mots-clés de la syntaxe des termes (i.e. en
   minuscules) pour les constructions similaires de tactiques (let_in,
-  match, and, etc.). Le connecteur logique \texttt{and} n'�tant que
-  rarement utilis� autrement que sous la forme \texttt{$\wedge$} (sauf
-  dans le code ML), on pourrait d�gager ce mot-cl�.
-\item Les arguments pass�s aux tactiques sont principalement des
-  termes, on pr�conise l'utilisation d'un symbole sp�cial (par exemple
+  match, and, etc.). Le connecteur logique \texttt{and} n'étant que
+  rarement utilisé autrement que sous la forme \texttt{$\wedge$} (sauf
+  dans le code ML), on pourrait dégager ce mot-clé.
+\item Les arguments passés aux tactiques sont principalement des
+  termes, on préconise l'utilisation d'un symbole spécial (par exemple
   l'apostrophe) pour passer une tactique ou une expression
-  (AST). L'id�e �tant que l'on �crit plus souvent des tactiques
+  (AST). L'idée étant que l'on écrit plus souvent des tactiques
   prenant des termes en argument que des tacticals.
 \end{itemize}
 
@@ -97,15 +97,15 @@ souhaite suivre.
 \subsection{Arguments de tactiques}
 
 La syntaxe actuelle des arguments de tactiques est que l'on parse par
-d�faut une expression de tactique, ou bien l'on parse un terme si
-celui-ci est pr�fix� par \TERM{'} (sauf dans le cas des
-variables). Cela est g�nant pour les utilisateurs qui doivent �crire
+défaut une expression de tactique, ou bien l'on parse un terme si
+celui-ci est préfixé par \TERM{'} (sauf dans le cas des
+variables). Cela est gênant pour les utilisateurs qui doivent écrire
 des \TERM{'} pour leurs tactiques.
 
-� mon avis, il n'est pas souhaitable pour l'utilisateur de l'obliger �
-marquer une diff�rence entre les tactiques ``primitives'' (en fait
-``syst�me'') et les tactiques d�finies par Ltac. En effet, on se
-dirige in�vitablement vers une situation o� il existera des librairies
+À mon avis, il n'est pas souhaitable pour l'utilisateur de l'obliger à
+marquer une différence entre les tactiques ``primitives'' (en fait
+``système'') et les tactiques définies par Ltac. En effet, on se
+dirige inévitablement vers une situation où il existera des librairies
 de tactiques et il va devenir difficile de savoir facilement s'il faut
 ou non mettre des \TERM{'}.
 
@@ -113,33 +113,33 @@ ou non mettre des \TERM{'}.
 
 \subsection{Bindings}
 
-Dans un premier temps, les ``bindings'' sont toujours consid�r�s comme
-une construction du langage des tactiques, mais il est int�ressant de
-pr�voir l'extension de ce proc�d� aux termes, puisqu'il s'agit
+Dans un premier temps, les ``bindings'' sont toujours considérés comme
+une construction du langage des tactiques, mais il est intéressant de
+prévoir l'extension de ce procédé aux termes, puisqu'il s'agit
 simplement de construire un n{\oe}ud d'application dans lequel on
-donne les arguments par nom ou par position, les autres restant �
-inf�rer. Le principal point est de trouver comment combiner de mani�re
-uniforme ce proc�d� avec les arguments implicites.
+donne les arguments par nom ou par position, les autres restant à
+inférer. Le principal point est de trouver comment combiner de manière
+uniforme ce procédé avec les arguments implicites.
 
-Il est toutefois important de r�fl�chir d�s maintenant � une syntaxe
-pour �viter de rechanger encore la syntaxe.
+Il est toutefois important de réfléchir dès maintenant à une syntaxe
+pour éviter de rechanger encore la syntaxe.
 
-Int�grer la notation \TERM{with} aux termes peut poser des probl�mes
-puisque ce mot-cl� est utilis� pour le filtrage: comment parser (en
+Intégrer la notation \TERM{with} aux termes peut poser des problèmes
+puisque ce mot-clé est utilisé pour le filtrage: comment parser (en
 LL(1)) l'expression:
 \begin{verbatim}
 Cases x with y ...
 \end{verbatim}
 
-Soit on trouve un autre mot-cl�, soit on joue avec les niveaus de
-priorit� en obligeant a parenth�ser le \TERM{with} des ``bindings'':
+Soit on trouve un autre mot-clé, soit on joue avec les niveaus de
+priorité en obligeant a parenthéser le \TERM{with} des ``bindings'':
 \begin{verbatim}
 Cases (x with y) with (C z) => ...
 \end{verbatim}
-ce qui introduit un constructeur moralement �quivalent � une
-application situ� � une priorit� totalement diff�rente (les
+ce qui introduit un constructeur moralement équivalent à une
+application situé à une priorité totalement différente (les
 ``bindings'' seraient au plus haut niveau alors que l'application est
-� un niveau bas).
+à un niveau bas).
 
 
 \begin{figure}
@@ -156,9 +156,9 @@ application situ� � une priorit� totalement diff�rente (les
 
 \subsection{Enregistrements}
 
-Il faudrait am�nager la syntaxe des enregistrements dans l'optique
-d'avoir des enregistrements anonymes (termes de premi�re classe), m�me
-si pour l'instant, on ne dispose que d'enregistrements d�finis a
+Il faudrait aménager la syntaxe des enregistrements dans l'optique
+d'avoir des enregistrements anonymes (termes de première classe), même
+si pour l'instant, on ne dispose que d'enregistrements définis a
 toplevel.
 
 Exemple de syntaxe pour les types d'enregistrements:
@@ -179,22 +179,22 @@ Exemple de syntaxe pour le constructeur:
   ...
 }
 \end{verbatim}
-Quant aux d�pendences, une convention pourrait �tre de consid�rer les
-champs non annot�s par le type comme non d�pendants.
+Quant aux dépendences, une convention pourrait être de considérer les
+champs non annotés par le type comme non dépendants.
 
 Plusieurs interrogations:
 \begin{itemize}
-\item l'ordre des champs doit-il �tre respect� ?
+\item l'ordre des champs doit-il être respecté ?
   sinon, que faire pour les champs sans projection ?
 \item autorise-t-on \texttt{v1} a mentionner \texttt{x1} (comme dans
-  la d�finition d'un module), ce qui se comporterait comme si on avait
-  �crit \texttt{v1} � la place. Cela pourrait �tre une autre mani�re
-  de d�clarer les d�pendences
+  la définition d'un module), ce qui se comporterait comme si on avait
+  écrit \texttt{v1} à la place. Cela pourrait être une autre manière
+  de déclarer les dépendences
 \end{itemize}
 
-La notation point�e pour les projections pose un probl�me de parsing,
+La notation pointée pour les projections pose un problème de parsing,
 sauf si l'on a une convention lexicale qui discrimine les noms de
-modules des projections et identificateurs: \texttt{x.y.z} peut �tre
+modules des projections et identificateurs: \texttt{x.y.z} peut être
 compris comme \texttt{(x.y).z} ou texttt{x.(y.z)}.
 
 
@@ -204,17 +204,17 @@ compris comme \texttt{(x.y).z} ou texttt{x.(y.z)}.
 \subsection{Quelques principes}
 
 \begin{enumerate}
-\item Diminuer le nombre de niveaux de priorit� en regroupant les
-  r�gles qui se ressemblent: infixes, pr�fixes, lieurs (constructions
-  ouvertes � droite), etc.
-\item �viter de surcharger la signification d'un symbole (ex:
-  \verb+( )+ comme parenth�sage et produit dans la V7).
+\item Diminuer le nombre de niveaux de priorité en regroupant les
+  règles qui se ressemblent: infixes, préfixes, lieurs (constructions
+  ouvertes à droite), etc.
+\item Éviter de surcharger la signification d'un symbole (ex:
+  \verb+( )+ comme parenthésage et produit dans la V7).
 \item Faire en sorte que les membres gauches (motifs de Cases, lieurs
   d'abstraction ou de produits) utilisent une syntaxe compatible avec
   celle des membres droits (branches de Cases et corps de fonction).
 \end{enumerate}
 
-\subsection{Pr�sentation de la grammaire}
+\subsection{Présentation de la grammaire}
 
 \begin{figure}
 \begin{rulebox}
@@ -286,15 +286,15 @@ compris comme \texttt{(x.y).z} ou texttt{x.(y.z)}.
 \label{gram-annexes}
 \end{figure}
 
-La grammaire des termes (correspondant � l'�tat \texttt{barestate})
-est d�crite figures~\ref{constr} et~\ref{gram-annexes}. On constate
-par rapport aux pr�c�dentes versions de Coq d'importants changements
-de priorit�, le plus marquant �tant celui de l'application qui se
-trouve d�sormais juste au dessus\footnote{La convention est de
-consid�rer les op�rateurs moins lieurs comme ``au dessus'',
-c'est-�-dire ayant un niveau de priorit� plus �l�v� (comme c'est le
+La grammaire des termes (correspondant à l'état \texttt{barestate})
+est décrite figures~\ref{constr} et~\ref{gram-annexes}. On constate
+par rapport aux précédentes versions de Coq d'importants changements
+de priorité, le plus marquant étant celui de l'application qui se
+trouve désormais juste au dessus\footnote{La convention est de
+considérer les opérateurs moins lieurs comme ``au dessus'',
+c'est-à-dire ayant un niveau de priorité plus élévé (comme c'est le
 cas avec le niveau de la grammaire actuelle des termes).} des
-constructions ferm�es � gauche et � droite.
+constructions fermées à gauche et à droite.
 
 La grammaire des noms globaux est la suivante:
 \begin{eqnarray*}
@@ -304,43 +304,43 @@ La grammaire des noms globaux est la suivante:
 \nlsep \NT{ident}\TERM{.}\NT{global}
 \end{eqnarray*}
 
-Le $\TERM{_}$ d�note les termes � synth�tiser. Les m�tavariables sont
+Le $\TERM{_}$ dénote les termes à synthétiser. Les métavariables sont
 reconnues au niveau du lexer pour ne pas entrer en conflit avec le
 $\TERM{?}$ de l'existentielle.
 
-Les op�rateurs infixes ou pr�fixes sont tous au m�me niveau de
-priorit� du point de vue de Camlp4. La solution envisag�e est de les
-g�rer � la mani�re de Yacc, avec une pile (voir discussions plus
+Les opérateurs infixes ou préfixes sont tous au même niveau de
+priorité du point de vue de Camlp4. La solution envisagée est de les
+gérer à la manière de Yacc, avec une pile (voir discussions plus
 bas). Ainsi, l'implication est un infixe normal; la quantification
-universelle et le let sont vus comme des op�rateurs pr�fixes avec un
-niveau de priorit� plus haut (i.e. moins lieur). Il subsiste des
-probl�mes si l'on ne veut pas �crire de parenth�ses dans:
+universelle et le let sont vus comme des opérateurs préfixes avec un
+niveau de priorité plus haut (i.e. moins lieur). Il subsiste des
+problèmes si l'on ne veut pas écrire de parenthèses dans:
 \begin{verbatim}
  A -> (!x. B -> (let y = C in D))
 \end{verbatim}
 
-La solution propos�e est d'analyser le membre droit d'un infixe de
-mani�re � autoriser les pr�fixes et les infixes de niveau inf�rieur,
-et d'exiger le parenth�sage que pour les infixes de niveau sup�rieurs.
+La solution proposée est d'analyser le membre droit d'un infixe de
+manière à autoriser les préfixes et les infixes de niveau inférieur,
+et d'exiger le parenthésage que pour les infixes de niveau supérieurs.
 
-En revanche, � l'affichage, certains membres droits seront plus
+En revanche, à l'affichage, certains membres droits seront plus
 lisibles s'ils n'utilisent pas cette astuce:
 \begin{verbatim}
 (fun x => x) = fun x => x
 \end{verbatim}
 
-La proposition est d'autoriser ce type d'�critures au parsing, mais
-l'afficheur �crit de mani�re standardis�e en mettant quelques
-parenth�ses superflues: $\TERM{=}$ serait sym�trique alors que
-$\rightarrow$ appellerait l'afficheur de priorit� �lev�e pour son
+La proposition est d'autoriser ce type d'écritures au parsing, mais
+l'afficheur écrit de manière standardisée en mettant quelques
+parenthèses superflues: $\TERM{=}$ serait symétrique alors que
+$\rightarrow$ appellerait l'afficheur de priorité élevée pour son
 sous-terme droit.
 
-Les priorit�s des op�rateurs primitifs sont les suivantes (le signe
-$*$ signifie que pour le membre droit les op�rateurs pr�fixes seront
-affich�s sans parenth�ses quel que soit leur priorit�):
+Les priorités des opérateurs primitifs sont les suivantes (le signe
+$*$ signifie que pour le membre droit les opérateurs préfixes seront
+affichés sans parenthèses quel que soit leur priorité):
 $$
 \begin{array}{c|l}
-$symbole$ & $priorit�$ \\
+$symbole$ & $priorité$ \\
 \hline
 \TERM{!}      & 200\,R* \\
 \TERM{fun}    & 200\,R* \\
@@ -351,39 +351,39 @@ $symbole$ & $priorit�$ \\
 \end{array}
 $$
 
-Il y a deux points d'entr�e pour les termes: $\NT{constr}$ et
-$\NT{simple-constr}$. Le premier peut �tre utilis� lorsqu'il est suivi
-d'un s�parateur particulier. Dans le cas o� l'on veut une liste de
-termes s�par�s par un espace, il faut lire des $\NT{simple-constr}$.
+Il y a deux points d'entrée pour les termes: $\NT{constr}$ et
+$\NT{simple-constr}$. Le premier peut être utilisé lorsqu'il est suivi
+d'un séparateur particulier. Dans le cas où l'on veut une liste de
+termes séparés par un espace, il faut lire des $\NT{simple-constr}$.
 
 
 
 Les constructions $\TERM{fix}$ et $\TERM{cofix}$ (voir aussi
-figure~\ref{gram-fix}) sont ferm�es par end pour simplifier
-l'analyse. Sinon, une expression de point fixe peut �tre suivie par un
-\TERM{in} ou un \TERM{and}, ce qui pose les m�mes probl�mes que le
+figure~\ref{gram-fix}) sont fermées par end pour simplifier
+l'analyse. Sinon, une expression de point fixe peut être suivie par un
+\TERM{in} ou un \TERM{and}, ce qui pose les mêmes problèmes que le
 ``dangling else'': dans
 \begin{verbatim}
 fix f1 x {x} = fix f2 y {y} = ... and ... in ...
 \end{verbatim}
-il faut d�finir une strat�gie pour associer le \TERM{and} et le
+il faut définir une stratégie pour associer le \TERM{and} et le
 \TERM{in} au bon point fixe.
 
 Un autre avantage est de faire apparaitre que le \TERM{fix} est un
-constructeur de terme de premi�re classe et pas un lieur:
+constructeur de terme de première classe et pas un lieur:
 \begin{verbatim}
 fix f1 ... and f2 ...
 in f1 end x
 \end{verbatim}
-Les propositions pr�c�dentes laissaient \texttt{f1} et \texttt{x}
-accol�s, ce qui est source de confusion lorsque l'on fait par exemple
+Les propositions précédentes laissaient \texttt{f1} et \texttt{x}
+accolés, ce qui est source de confusion lorsque l'on fait par exemple
 \texttt{Pattern (f1 x)}.
 
 Les corps de points fixes et co-points fixes sont identiques, bien que
-ces derniers n'aient pas d'information de d�croissance. Cela
-fonctionne puisque l'annotation est optionnelle. Cela pr�figure des
-cas o� l'on arrive � inf�rer quel est l'argument qui d�croit
-structurellement (en particulier dans le cas o� il n'y a qu'un seul
+ces derniers n'aient pas d'information de décroissance. Cela
+fonctionne puisque l'annotation est optionnelle. Cela préfigure des
+cas où l'on arrive à inférer quel est l'argument qui décroit
+structurellement (en particulier dans le cas où il n'y a qu'un seul
 argument).
 
 \begin{figure}
@@ -412,8 +412,8 @@ argument).
 \label{gram-fix}
 \end{figure}
 
-La construction $\TERM{Case}$ peut-�tre consid�r�e comme
-obsol�te. Quant au $\TERM{Match}$ de la V6, il dispara�t purement et
+La construction $\TERM{Case}$ peut-être considérée comme
+obsolète. Quant au $\TERM{Match}$ de la V6, il disparaît purement et
 simplement.
 
 \begin{figure}
@@ -456,15 +456,15 @@ simplement.
 \label{gram-match}
 \end{figure}
 
-De mani�re globale, l'introduction de d�finitions dans les termes se
-fait avec le symbole $=$, et le $\!:=$ est r�serv� aux d�finitions au
-niveau vernac. Il y avait un manque de coh�rence dans la
+De manière globale, l'introduction de définitions dans les termes se
+fait avec le symbole $=$, et le $\!:=$ est réservé aux définitions au
+niveau vernac. Il y avait un manque de cohérence dans la
 V6, puisque l'on utilisait $=$ pour le $\TERM{let}$ et $\!:=$ pour les
 points fixes et les commandes vernac.
 
 % OBSOLETE: lieurs multiples supprimes
 %On peut remarquer que $\NT{binder}$ est un sous-ensemble de
-%$\NT{simple-constr}$, � l'exception de $\texttt{(a,b\!\!:T)}$: en tant
+%$\NT{simple-constr}$, à l'exception de $\texttt{(a,b\!\!:T)}$: en tant
 %que lieur, {\tt a} et {\tt b} sont tous deux contraints, alors qu'en
 %tant que terme, seul {\tt b} l'est. Cela qui signifie que l'objectif
 %de rendre compatibles les membres gauches et droits est {\it presque}
@@ -474,14 +474,14 @@ points fixes et les commandes vernac.
 
 \subsubsection{Infixes extensibles}
 
-Le probl�me de savoir si la liste des symboles pouvant appara�tre en
-infixe est fix�e ou extensible par l'utilisateur reste � voir.
+Le problème de savoir si la liste des symboles pouvant apparaître en
+infixe est fixée ou extensible par l'utilisateur reste à voir.
 
-Notons que la solution o� les symboles infixes sont des
-identificateurs que l'on peut d�finir para�t difficilement praticable:
-par exemple $\texttt{Logic.eq}$ n'est pas un op�rateur binaire, mais
-ternaire. Il semble plus simple de garder des d�clarations infixes qui
-relient un symbole infixe � un terme avec deux ``trous''. Par exemple:
+Notons que la solution où les symboles infixes sont des
+identificateurs que l'on peut définir paraît difficilement praticable:
+par exemple $\texttt{Logic.eq}$ n'est pas un opérateur binaire, mais
+ternaire. Il semble plus simple de garder des déclarations infixes qui
+relient un symbole infixe à un terme avec deux ``trous''. Par exemple:
 
 $$\begin{array}{c|l}
 $infixe$ &  $identificateur$ \\
@@ -490,33 +490,33 @@ $infixe$ &  $identificateur$ \\
 == & \texttt{JohnMajor.eq _ ?1 _ ?2}
 \end{array}$$
 
-La syntaxe d'une d�claration d'infixe serait par exemple:
+La syntaxe d'une déclaration d'infixe serait par exemple:
 \begin{verbatim}
 Infix "=" 50 := Logic.eq _ ?1 ?2;
 \end{verbatim}
 
 
-\subsubsection{Gestion des pr�c�dences}
+\subsubsection{Gestion des précédences}
 
-Les infixes peuvent �tre soit laiss� � Camlp4, ou bien (comme ici)
-consid�rer que tous les op�rateurs ont la m�me pr�c�dence et g�rer
-soit m�me la recomposition des termes � l'aide d'une pile (comme
+Les infixes peuvent être soit laissé à Camlp4, ou bien (comme ici)
+considérer que tous les opérateurs ont la même précédence et gérer
+soit même la recomposition des termes à l'aide d'une pile (comme
 Yacc).
 
 
 \subsection{Extensions de syntaxe}
 
-\subsubsection{Lit�raux num�riques}
+\subsubsection{Litéraux numériques}
 
-La proposition est de considerer les lit�raux num�riques comme de
-simples identificateurs. Comme il en existe une infinit�, il faut un
-nouveau m�canisme pour leur associer une d�finition. Par exemple, en
-ce qui concerne \texttt{Arith}, la d�finition de $5$ serait
+La proposition est de considerer les litéraux numériques comme de
+simples identificateurs. Comme il en existe une infinité, il faut un
+nouveau mécanisme pour leur associer une définition. Par exemple, en
+ce qui concerne \texttt{Arith}, la définition de $5$ serait
 $\texttt{S}~4$. Pour \texttt{ZArith}, $5$ serait $\texttt{xI}~2$.
 
-Comme les infixes, les constantes num�riques peuvent �tre qualifi�es
+Comme les infixes, les constantes numériques peuvent être qualifiées
 pour indiquer dans quels module est le type que l'on veut
-r�f�rencer. Par exemple (si on renomme \texttt{Arith} en \texttt{N} et
+référencer. Par exemple (si on renomme \texttt{Arith} en \texttt{N} et
 \texttt{ZArith} en \texttt{Z}): \verb+N.5+, \verb+Z.5+.
 
 \begin{eqnarray*}
@@ -539,18 +539,18 @@ $$
 $$
 
 Pour l'instant l'existentielle n'admet qu'une seule variable, ce qui
-oblige � �crire des cascades de $\TERM{ex}$.
+oblige à écrire des cascades de $\TERM{ex}$.
 
-Pour parser les existentielles avec deux pr�dicats, on peut consid�rer
-\TERM{\&} comme un infixe interm�diaire et l'op�rateur existentiel en
-pr�sence de cet infixe se transforme en \texttt{ex2}.
+Pour parser les existentielles avec deux prédicats, on peut considérer
+\TERM{\&} comme un infixe intermédiaire et l'opérateur existentiel en
+présence de cet infixe se transforme en \texttt{ex2}.
 
 \subsubsection{Nouveaux infixes}
 
-Pr�c�dences des op�rateurs infixes (les plus grands associent moins fort):
+Précédences des opérateurs infixes (les plus grands associent moins fort):
 $$
 \begin{array}{l|l|c|l}
-$identificateur$      & $module$     & $infixe/pr�fixe$ & $pr�c�dence$ \\
+$identificateur$      & $module$     & $infixe/préfixe$ & $précédence$ \\
 \hline
 \texttt{iff}          & $Logic$      & \longleftrightarrow & 100 \\
 \texttt{or}           & $Logic$      & \vee     & 80\, R \\
@@ -590,8 +590,8 @@ $identificateur$      & $module$     & $infixe/pr�fixe$ & $pr�c�dence$ \\
 \end{array}
 $$
 
-Notons qu'il faudrait d�couper {\tt Logic_Type} en deux car celui-ci
-d�finit deux �galit�s, ou alors les mettre dans des modules diff�rents.
+Notons qu'il faudrait découper {\tt Logic_Type} en deux car celui-ci
+définit deux égalités, ou alors les mettre dans des modules différents.
 
 \subsection{Exemples}
 
@@ -611,20 +611,20 @@ Fixpoint plus n m : nat {struct n} :=
 
 \subsection{Questions ouvertes}
 
-Voici les points sur lesquels la discussion est particuli�rement
+Voici les points sur lesquels la discussion est particulièrement
 ouverte: 
 \begin{itemize}
 \item choix d'autres symboles pour les quantificateurs \TERM{!} et
-  \TERM{?}. En l'�tat actuel des discussions, on garderait le \TERM{!}
+  \TERM{?}. En l'état actuel des discussions, on garderait le \TERM{!}
   pour la qunatification universelle, mais on choisirait quelquechose
-  comme \TERM{ex} pour l'existentielle, afin de ne pas sugg�rer trop
-  de sym�trie entre ces quantificateurs (l'un est primitif, l'autre
+  comme \TERM{ex} pour l'existentielle, afin de ne pas suggérer trop
+  de symétrie entre ces quantificateurs (l'un est primitif, l'autre
   pas).
-\item syntaxe particuli�re pour les \texttt{sig}, \texttt{sumor}, etc.
-\item la possibilit� d'introduire plusieurs variables du m�me type est
-  pour l'instant supprim�e au vu des probl�mes de compatibilit� de
-  syntaxe entre les membres gauches et membres droits. L'id�e �tant
-  que l'inference de type permet d'�viter le besoin de d�clarer tous
+\item syntaxe particulière pour les \texttt{sig}, \texttt{sumor}, etc.
+\item la possibilité d'introduire plusieurs variables du même type est
+  pour l'instant supprimée au vu des problèmes de compatibilité de
+  syntaxe entre les membres gauches et membres droits. L'idée étant
+  que l'inference de type permet d'éviter le besoin de déclarer tous
   les types.
 \end{itemize}
 
@@ -632,19 +632,19 @@ ouverte:
 
 \subsubsection{Lieur multiple}
 
-L'�criture de types en pr�sence de polymorphisme est souvent assez
-p�nible:
+L'écriture de types en présence de polymorphisme est souvent assez
+pénible:
 \begin{verbatim}
 Check !(A:Set) (x:A) (B:Set) (y:B). P A x B y;
 \end{verbatim}
 
-On pourrait avoir des d�clarations introduisant � la fois un type
+On pourrait avoir des déclarations introduisant à la fois un type
 d'une certaine sorte et une variable de ce type:
 \begin{verbatim}
 Check !(x:A:Set) (y:B:Set). P A x B y;
 \end{verbatim}
 
-Noter que l'on aurait pu �crire:
+Noter que l'on aurait pu écrire:
 \begin{verbatim}
 Check !A x B y. P A (x:A:Set) B (y:B:Set);
 \end{verbatim}
@@ -654,19 +654,19 @@ Check !A x B y. P A (x:A:Set) B (y:B:Set);
 \subsection{Questions diverses}
 
 Changer ``Pattern nl c ... nl c'' en ``Pattern [ nl ] c ... [ nl ] c''
-pour permettre des chiffres seuls dans la cat�gorie syntaxique des
+pour permettre des chiffres seuls dans la catégorie syntaxique des
 termes.
 
-Par uniformit� remplacer ``Unfold nl c'' par ``Unfold [ nl ] c'' ?
+Par uniformité remplacer ``Unfold nl c'' par ``Unfold [ nl ] c'' ?
 
-M�me probl�me pour l'entier de Specialize (ou virer Specialize ?) ?
+Même problème pour l'entier de Specialize (ou virer Specialize ?) ?
 
 \subsection{Questions en suspens}
 
-\verb=EAuto= : deux syntaxes diff�rentes pour la recherche en largeur
-et en profondeur ? Quelle recherche par d�faut ?
+\verb=EAuto= : deux syntaxes différentes pour la recherche en largeur
+et en profondeur ? Quelle recherche par défaut ?
 
-\section*{Remarques p�le-m�le (HH)}
+\section*{Remarques pêle-mêle (HH)}
 
 Autoriser la syntaxe
 
@@ -685,16 +685,16 @@ Mettre des \verb=?x= plutot que des \verb=?1= dans les motifs de ltac ??
 
 \begin{itemize}
 
-\item Mettre \verb=/= et * au m�me niveau dans R.
+\item Mettre \verb=/= et * au même niveau dans R.
 
-\item Changer la pr�c�dence du - unaire dans R.
+\item Changer la précédence du - unaire dans R.
 
 \item Ajouter Require Arith par necessite si Require ArithRing ou Require ZArithRing.
 
 \item Ajouter Require ZArith par necessite si Require ZArithRing ou Require Omega.
 
-\item Enlever le Export de Bool, Arith et ZARith de Ring quand inappropri� et
-l'ajouter � c�t� des Require Ring.
+\item Enlever le Export de Bool, Arith et ZARith de Ring quand inapproprié et
+l'ajouter à côté des Require Ring.
 
 \item Remplacer "Check n" par "n:Check ..."
 
diff --git a/dev/doc/old_svn_branches.txt b/dev/doc/old_svn_branches.txt
new file mode 100644
index 00000000..ee56ee24
--- /dev/null
+++ b/dev/doc/old_svn_branches.txt
@@ -0,0 +1,33 @@
+## During the migration to git, some old branches and tags have not been
+## converted to directly visible git branches or tags. They are still there
+## in the archive, their names on the gforge repository are in the 3rd
+## column below (e.g. remotes/V8-0-bugfix). After a git clone, they
+## could always be accessed by their git hashref (2nd column below).
+
+# SVN   # GIT   # Symbolic name on gforge repository
+
+r5      d2f789d remotes/tags/start
+r1714   0605b7c remotes/V7
+r2583   372f3f0 remotes/tags/modules-2-branching
+r2603   6e15d9a remotes/modules
+r2866   76a93fa remotes/tags/modules-2-before-grammar
+r2951   356f749 remotes/tags/before-modules
+r2952   8ee67df remotes/tags/modules-2-update
+r2956   fb11bd9 remotes/modules-2
+r3193   4d23172 remotes/mowgli
+r3194   c91e99b remotes/tags/mowgli-before-merge
+r3500   5078d29 remotes/mowgli2
+r3672   63b0886 remotes/V7-3-bugfix
+r5086   bdceb72 remotes/V7-4-bugfix
+r5731   a274456 remotes/recriture
+r9046   e19553c remotes/tags/trunk
+r9146   b38ce05 remotes/coq-diff-tool
+r9786   a05abf8 remotes/ProofIrrelevance
+r10294  fdf8871 remotes/InternalExtraction
+r10408  df97909 remotes/TypeClasses
+r10673  4e19bca remotes/bertot
+r11130  bfd1cb3 remotes/proofs
+r12282  a726b30 remotes/revised-theories
+r13855  bae3a8e remotes/native
+r14062  b77191b remotes/recdef
+r16421  9f4bfa8 remotes/V8-0-bugfix
diff --git a/dev/doc/patch.ocaml-3.10.drop.rectypes b/dev/doc/patch.ocaml-3.10.drop.rectypes
deleted file mode 100644
index ba7a3e95..00000000
--- a/dev/doc/patch.ocaml-3.10.drop.rectypes
+++ /dev/null
@@ -1,31 +0,0 @@
-Index: scripts/coqmktop.ml
-===================================================================
---- scripts/coqmktop.ml	(révision 12084)
-+++ scripts/coqmktop.ml	(copie de travail)
-@@ -231,12 +231,25 @@
-      end;;
- 
-      let ppf = Format.std_formatter;;
-+     let set_rectypes_hack () =
-+       if String.length (Sys.ocaml_version) >= 4 &
-+          String.sub (Sys.ocaml_version) 0 4 = \"3.10\"
-+       then
-+         (* ocaml 3.10 does not have #rectypes but needs it *)
-+         (* simulate a call with option -rectypes before *)
-+         (* jumping to the ocaml toplevel *)
-+         for i = 1 to Array.length Sys.argv - 1 do
-+           Sys.argv.(i) <- \"-rectypes\"
-+         done
-+       else
-+         () in
-+
-      Mltop.set_top
-        {Mltop.load_obj=
-          (fun f -> if not (Topdirs.load_file ppf f) then failwith \"error\");
-         Mltop.use_file=Topdirs.dir_use ppf;
-         Mltop.add_dir=Topdirs.dir_directory;
--        Mltop.ml_loop=(fun () -> Toploop.loop ppf) };;\n"
-+        Mltop.ml_loop=(fun () -> set_rectypes_hack(); Topmain.main()) };;\n"
- 
- (* create a temporary main file to link *)
- let create_tmp_main_file modules =
diff --git a/dev/doc/style.txt b/dev/doc/style.txt
index a8924ba6..27695a09 100644
--- a/dev/doc/style.txt
+++ b/dev/doc/style.txt
@@ -1,16 +1,16 @@
 
-<< L'uniformit� du style est plus importante que le style lui-m�me. >>
+<< L'uniformité du style est plus importante que le style lui-même. >>
 (Kernigan & Pike, The Practice of Programming)
 
 Mode Emacs
 ==========
    Tuareg, que l'on trouve ici :  http://www.prism.uvsq.fr/~acohen/tuareg/
 
-   avec le r�glage suivant :     (setq tuareg-in-indent 2)
+   avec le réglage suivant :     (setq tuareg-in-indent 2)
 
-Types r�cursifs et filtrages
+Types récursifs et filtrages
 ============================
-   Une barre de s�paration y compris sur le premier constructeur
+   Une barre de séparation y compris sur le premier constructeur
 
 type t =
   | A 
@@ -20,9 +20,9 @@ match expr with
   | A -> ...
   | B x -> ...
 
-Remarque : � partir de la 8.2 environ, la tendance est � utiliser le
+Remarque : à partir de la 8.2 environ, la tendance est à utiliser le
 format suivant qui permet de limiter l'escalade d'indentation tout en
-produisant un aspect visuel int�ressant de bloc :
+produisant un aspect visuel intéressant de bloc :
 
 type t =
 | A 
@@ -40,11 +40,11 @@ let f expr = function
 | A -> ...
 | B x -> ...
 
-Le deuxi�me cas est obtenu sous tuareg avec les r�glages
+Le deuxième cas est obtenu sous tuareg avec les réglages
 
   (setq tuareg-with-indent 0)
   (setq tuareg-function-indent 0)
-  (setq tuareg-let-always-indent nil) /// notons que cette derni�re est bien 
+  (setq tuareg-let-always-indent nil) /// notons que cette dernière est bien 
                                       /// pour les let mais pas pour les let-in
 
 Conditionnelles
@@ -55,7 +55,7 @@ Conditionnelles
     deuxieme-cas
 
   Si effets de bord dans les branches, utilisez begin ... end et non des
-  parenth�ses i.e.
+  parenthèses i.e.
 
   if condition then begin
     instr1;
@@ -65,7 +65,7 @@ Conditionnelles
     instr4
   end
     
-  Si la premi�re branche l�ve une exception, �vitez le else i.e.
+  Si la première branche lève une exception, évitez le else i.e.
 
     if condition then                     if condition then error "machin";
       error "machin"          ----->      suite
diff --git a/dev/doc/transition-V5.10-V6 b/dev/doc/transition-V5.10-V6
new file mode 100644
index 00000000..df7b65dd
--- /dev/null
+++ b/dev/doc/transition-V5.10-V6
@@ -0,0 +1,5 @@
+The V5.10 archive has been created with cvs in February 1995 by
+Jean-Christophe Filliâtre. It was moved to archive V6 in March 1996.
+At this occasion, the contrib directory (user-contributions) were
+moved to a separate directory and some theories (like ALGEBRA) moved
+to the user-contributions directory too.
diff --git a/dev/doc/transition-V6-V7 b/dev/doc/transition-V6-V7
new file mode 100644
index 00000000..e477c9ff
--- /dev/null
+++ b/dev/doc/transition-V6-V7
@@ -0,0 +1,8 @@
+The V6 archive has been created in March 1996 with files from the
+former V5.10 archive and has been abandoned in 2000.
+
+A new archive named V7 has been created in August 1999 by
+Jean-Christophe Filliâtre with a new architecture placing the
+type-checking at the kernel of Coq. This new architecture came with a
+"cleaner" organization of files, a uniform indentation style, uniform
+headers, etc.
diff --git a/dev/doc/univpoly.txt b/dev/doc/univpoly.txt
new file mode 100644
index 00000000..4c89af01
--- /dev/null
+++ b/dev/doc/univpoly.txt
@@ -0,0 +1,255 @@
+Notes on universe polymorphism and primitive projections, M. Sozeau - WIP 
+=========================================================================
+
+The new implementation of universe polymorphism and primitive
+projections introduces a few changes to the API of Coq. First and
+foremost, the term language changes, as global references now carry a
+universe level substitution:
+
+type 'a puniverses = 'a * Univ.Instance.t
+type pconstant = constant puniverses
+type pinductive = inductive puniverses
+type pconstructor = constructor puniverses
+
+type constr = ...
+  | Const of puniversess
+  | Ind of pinductive
+  | Constr of pconstructor
+  | Proj of constant * constr
+
+
+Universes
+=========
+
+  Universe instances (an array of levels) gets substituted when
+unfolding definitions, are used to typecheck and are unified according
+to the rules in the ITP'14 paper on universe polymorphism in Coq.  
+
+type Level.t = Set | Prop | Level of int * dirpath (* hashconsed *)
+type Instance.t = Level.t array
+type Universe.t = Level.t list (* hashconsed *)
+
+The universe module defines modules and abstract types for levels,
+universes etc.. Structures are hashconsed (with a hack to take care
+of the fact that deserialization breaks sharing). 
+
+  Definitions (constants, inductives) now carry around not only 
+constraints but also the universes they introduced (a Univ.UContext.t).
+There is another kind of contexts [Univ.ContextSet.t], the latter has 
+a set of universes, while the former has serialized the levels in an
+array, and is used for polymorphic objects. Both have "reified" 
+constraints depending on global and local universes. 
+
+  A polymorphic definition is abstract w.r.t. the variables in this
+context, while a monomorphic one (or template polymorphic) just adds the
+universes and constraints to the global universe context when it is put
+in the environment. No other universes than the global ones and the
+declared local ones are needed to check a declaration, hence the kernel
+does not produce any constraints anymore, apart from module
+subtyping.... There are hance two conversion functions now: check_conv
+and infer_conv: the former just checks the definition in the current env
+(in which we usually push_universe_context of the associated context),
+and infer_conv which produces constraints that were not implied by the
+ambient constraints. Ideally, that one could be put out of the kernel,
+but again, module subtyping needs it. 
+
+ Inference of universes is now done during refinement, and the evar_map
+carries the incrementally built universe context. [Evd.conversion] is a
+wrapper around [infer_conv] that will do the bookkeeping for you, it
+uses [evar_conv_x]. There is a universe substitution being built
+incrementally according to the constraints, so one should normalize at
+the end of a proof (or during a proof) with that substitution just like
+we normalize evars. There are some nf_* functions in
+library/universes.ml to do that. Additionally, there is a minimization
+algorithm in there that can be applied at the end of a proof to simplify
+the universe constraints used in the term. It is heuristic but
+validity-preserving. No user-introduced universe (i.e. coming from a
+user-written anonymous Type) gets touched by this, only the fresh
+universes generated for each global application. Using
+
+val pf_constr_of_global : Globnames.global_reference -> (constr -> tactic) -> tactic
+
+Is the way to make a constr out of a global reference in the new API.
+If they constr is polymorphic, it will add the necessary constraints to
+the evar_map. Even if a constr is not polymorphic, we have to take care
+of keeping track of it's universes. Typically, using:
+
+  mkApp (coq_id_function, [| A; a |]) 
+
+and putting it in a proof term is not enough now. One has to somehow
+show that A's type is in cumululativity relation with id's type
+argument, incurring a universe constraint. To do this, one can simply
+call Typing.resolve_evars env evdref c which will do some infer_conv to
+produce the right constraints and put them in the evar_map. Of course in
+some cases you might now from an invariant that no new constraint would
+be produced and get rid of it. Anyway the kernel will tell you if you
+forgot some. As a temporary way out, [Universes.constr_of_global] allows
+you to make a constr from any non-polymorphic constant, but it might
+forget constraints.
+
+Other than that, unification (w_unify and evarconv) now take account of universes and
+produce only well-typed evar_maps.
+
+Some syntactic comparisons like the one used in [change] have to be
+adapted to allow identification up-to-universes (when dealing with 
+polymorphic references), [make_eq_univs_test] is there to help. 
+In constr, there are actually many new comparison functions to deal with
+that:
+ 
+(** [equal a b] is true if [a] equals [b] modulo alpha, casts,
+   and application grouping *)
+val equal : constr -> constr -> bool
+
+(** [eq_constr_univs u a b] is [true] if [a] equals [b] modulo alpha, casts,
+   application grouping and the universe equalities in [u]. *)
+val eq_constr_univs : constr Univ.check_function
+
+(** [leq_constr_univs u a b] is [true] if [a] is convertible to [b] modulo 
+    alpha, casts, application grouping and the universe inequalities in [u]. *)
+val leq_constr_univs : constr Univ.check_function
+
+(** [eq_constr_universes a b] [true, c] if [a] equals [b] modulo alpha, casts,
+   application grouping and the universe equalities in [c]. *)
+val eq_constr_universes : constr -> constr -> bool Univ.universe_constrained
+
+(** [leq_constr_universes a b] [true, c] if [a] is convertible to [b] modulo
+    alpha, casts, application grouping and the universe inequalities in [c]. *)
+val leq_constr_universes : constr -> constr -> bool Univ.universe_constrained
+
+(** [eq_constr_univs a b] [true, c] if [a] equals [b] modulo alpha, casts,
+   application grouping and ignoring universe instances. *)
+val eq_constr_nounivs : constr -> constr -> bool
+
+The [_univs] versions are doing checking of universe constraints
+according to a graph, while the [_universes] are producing (non-atomic) 
+universe constraints. The non-atomic universe constraints include the
+[ULub] constructor: when comparing [f (* u1 u2 *) c] and [f (* u1' u2'
+*) c] we add ULub constraints on [u1, u1'] and [u2, u2']. These are
+treated specially: as unfolding [f] might not result in these
+unifications, we need to keep track of the fact that failure to satisfy
+them does not mean that the term are actually equal. This is used in
+unification but probably not necessary to the average programmer. 
+
+Another issue for ML programmers is that tables of constrs now usually
+need to take a [constr Univ.in_universe_context_set] instead, and
+properly refresh the universes context when using the constr, e.g. using 
+Clenv.refresh_undefined_univs clenv or: 
+
+(** Get fresh variables for the universe context.
+    Useful to make tactics that manipulate constrs in universe contexts polymorphic. *)
+val fresh_universe_context_set_instance : universe_context_set -> 
+  universe_level_subst * universe_context_set
+
+The substitution should be applied to the constr(s) under consideration, 
+and the context_set merged with the current evar_map with:
+
+val merge_context_set : rigid -> evar_map -> Univ.universe_context_set -> evar_map
+
+The [rigid] flag here should be [Evd.univ_flexible] most of the
+time. This means the universe levels of polymorphic objects in the
+constr might get instantiated instead of generating equality constraints 
+(Evd.univ_rigid does that).
+
+On this issue, I recommend forcing commands to take [global_reference]s
+only, the user can declare his specialized terms used as hints as
+constants and this is cleaner. Alas, backward-compatibility-wise,
+this is the only solution I found. In the case of global_references
+only, it's just a matter of using [Evd.fresh_global] /
+[pf_constr_of_global] to let the system take care of universes.
+
+Projections
+===========
+
+  | Proj of constant * constr
+
+Projections are always applied to a term, which must be of a record type
+(i.e. reducible to an inductive type [I params]). Type-checking,
+reduction and conversion are fast (not as fast as they could be yet)
+because we don't keep parameters around. As you can see, it's currently
+a [constant] that is used here to refer to the projection, that will
+change to an abstract [projection] type in the future. Basically a
+projection constant records which inductive it is a projection for, the
+number of params and the actual position in the constructor that must be
+projected. For compatibility reason, we also define an eta-expanded form
+(accessible from user syntax @f). The constant_entry of a projection has
+both informations. Declaring a record (under [Set Primitive
+Projections]) will generate such definitions. The API to declare them is
+not stable at the moment, but the inductive type declaration also knows
+about the projections, i.e. a record inductive type decl contains an
+array of terms representing the projections. This is used to implement
+eta-conversion for record types (with at least one field and having all
+projections definable). The canonical value being [Build_R (pn x)
+... (pn x)]. Unification and conversion work up to this eta rule. The
+records can also be universe polymorphic of course, and we don't need to
+keep track of the universe instance for the projections either.
+Projections are reduced _eagerly_ everywhere, and introduce a new Zproj
+constructor in the abstract machines that obeys both the delta (for the
+constant opacity) and iota laws (for the actual reduction). Refolding
+works as well (afaict), but there is a slight hack there related to
+universes (not projections). 
+
+For the ML programmer, the biggest change is that pattern-matchings on
+kind_of_term require an additional case, that is handled usually exactly
+like an [App (Const p) arg].
+
+There are slight hacks related to hints is well, to use the primitive
+projection form of f when one does [Hint Resolve f]. Usually hint
+resolve will typecheck the term, resulting in a partially applied
+projection (disallowed), so we allow it to take
+[constr_or_global_reference] arguments instead and special-case on
+projections. Other tactic extensions might need similar treatment. 
+
+WIP
+===
+
+- [vm_compute] does not deal with universes and projections correctly,
+except when it goes to a normal form with no projections or polymorphic
+constants left (the most common case). E.g. Ring with Set Universe
+Polymorphism and Set Primitive Projections work (at least it did at some
+point, I didn't recheck yet).  
+
+- [native_compute] is untested: it should deal with primitive
+projections right but not universes.
+
+
+Incompatibilities
+=================
+
+Old-style universe polymorphic definitions were implemented by taking
+advantage of the fact that elaboration (i.e., pretyping and unification)
+were _not_ universe aware, so some of the constraints generated during
+pretypechecking would be forgotten. In the current setting, this is not
+possible, as unification ensures that the substitution is built is
+entirely well-typed, even w.r.t universes. This means that some terms
+that type-checked before no longer do, especially projections of the
+pair:
+
+@fst ?x ?y : prod ?x ?y : Type (max(Datatypes.i, Datatypes.j)).
+
+The "template universe polymorphic" variables i and j appear during
+typing without being refreshed, meaning that they can be lowered (have
+upper constraints) with user-introduced universes. In most cases this
+won't work, so ?x and ?y have to be instantiated earlier, either from
+the type of the actual projected pair term (some t : prod A B) or the
+typing constraint. Adding the correct type annotations will always fix 
+this.
+
+
+Unification semantics
+=====================
+
+In Ltac, matching with:
+
+- a universe polymorphic constant [c] matches any instance of the
+  constant.
+- a variable ?x already bound to a term [t] (non-linear pattern) uses 
+  strict equality of universes (e.g., Type@{i} and Type@{j} are not
+  equal).
+
+In tactics:
+
+- [change foo with bar], [pattern foo] will unify all instances of [foo]
+  (and convert them with [bar]). This might incur unifications of
+  universes. [change] uses conversion while [pattern] only does
+  syntactic matching up-to unification of universes.
+- [apply], [refine] use unification up to universes.
diff --git a/dev/doc/versions-history.tex b/dev/doc/versions-history.tex
index 175297f9..9892a441 100644
--- a/dev/doc/versions-history.tex
+++ b/dev/doc/versions-history.tex
@@ -1,6 +1,6 @@
 \documentclass[a4paper]{book}
 \usepackage{fullpage}
-\usepackage[latin1]{inputenc}
+\usepackage[utf8]{inputenc}
 \usepackage[T1]{fontenc}
 \usepackage{amsfonts}
 
@@ -245,7 +245,7 @@ Coq V6.3.1& released 7 December 1999\\
 \begin{tabular}{l|l|l}
 version & date & comments \\
 \hline
-Coq ``V7'' archive & August 1999 & new cvs archive based on J.-C. Filli�tre's \\
+Coq ``V7'' archive & August 1999 & new cvs archive based on J.-C. Filliâtre's \\
    & & \feature{kernel-centric} architecture \\
    & & more care for outside readers\\
    & & (indentation, ocaml warning protection)\\