Imported Upstream version 8.5~beta1+dfsg

30 files changed, 2080 insertions, 700 deletions

diff --git a/dev/TODO b/dev/TODO
index 926861c9..e62ee6e5 100644
--- a/dev/TODO
+++ b/dev/TODO
@@ -3,16 +3,16 @@
      - reporter les options de l'ancien script coqtop sur le nouveau coqtop.ml
 
  o arguments implicites
-     - les calculer une fois pour toutes à la déclaration (dans Declare)
+     - les calculer une fois pour toutes à la déclaration (dans Declare)
        et stocker cette information dans le in_variable, in_constant, etc.
 
- o Environnements compilés (type Environ.compiled_env)
-     - pas de timestamp mais plutôt un checksum avec Digest (mais comment ?)
+ o Environnements compilés (type Environ.compiled_env)
+     - pas de timestamp mais plutôt un checksum avec Digest (mais comment ?)
 
- o Efficacité
-     - utiliser DOPL plutôt que DOPN (sauf pour Case)
+ o Efficacité
+     - utiliser DOPL plutôt que DOPN (sauf pour Case)
      - batch mode => pas de undo, ni de reset
-     - conversion : déplier la constante la plus récente
+     - conversion : déplier la constante la plus récente
      - un cache pour type_of_const, type_of_inductive, type_of_constructor,
        lookup_mind_specif
 
diff --git a/dev/base_include b/dev/base_include
index 9a788b7b..de63c557 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -12,7 +12,10 @@
 #directory "lib";;
 #directory "proofs";;
 #directory "tactics";;
-#directory "translate";;
+#directory "printing";;
+#directory "grammar";;
+#directory "intf";;
+#directory "stm";;
 
 #directory "+camlp4";; (* lazy solution: add both of camlp4/5 so that *)
 #directory "+camlp5";; (* Gramext is found in top_printers.ml *)
@@ -31,14 +34,17 @@
 #install_printer  (* qualid *)  ppqualid;;
 #install_printer  (* kernel_name *) ppkn;;
 #install_printer  (* constant *) ppcon;;
+#install_printer  (* projection *) ppproj;;
 #install_printer  (* cl_index *) ppclindex;;
-#install_printer  (* constr *)  print_pure_constr;; 
+#install_printer  (* recarg Rtree.t *)  ppwf_paths;;
+#install_printer  (* constr *)  print_pure_constr;;
 #install_printer  (* patch *) ppripos;;
 #install_printer  (* values *) ppvalues;;
 #install_printer  (* Idpred.t *) pp_idpred;;
 #install_printer  (* Cpred.t *) pp_cpred;;
 #install_printer ppzipper;;
 #install_printer ppstack;;
+#install_printer (* Reductionops.Stack.t *) pp_stack_t;;
 #install_printer ppatom;;
 #install_printer ppwhd;;
 #install_printer ppvblock;;
@@ -50,6 +56,8 @@
 
 open Names
 open Term
+open Vars
+open Context
 open Typeops
 open Term_typing
 open Univ
@@ -63,38 +71,48 @@ open Declare
 open Declaremods
 open Impargs
 open Libnames
+open Globnames
 open Nametab
 open Library
 
 open Cases
 open Pattern
+open Patternops
 open Cbv
 open Classops
+open Arguments_renaming
 open Pretyping
-open Pretyping.Default
-open Pretyping.Default.Cases
 open Cbv
 open Classops
 open Clenv
 open Clenvtac
 open Glob_term
+open Glob_ops
 open Coercion
-open Coercion.Default
 open Recordops
 open Detyping
 open Reductionops
 open Evarconv
 open Retyping
 open Evarutil
+open Evarsolve
 open Tacred
 open Evd
+open Universes
 open Termops
 open Namegen
 open Indrec
 open Typing
 open Inductiveops
+open Locusops
+open Find_subterm
 open Unification
-open Matching
+open Miscops
+open Miscops
+open Nativenorm
+open Typeclasses
+open Typeclasses_errors
+open Vnorm
 
 open Constrextern
 open Constrintern
@@ -105,19 +123,28 @@ open Notation
 open Ppextend
 open Reserve
 open Syntax_def
+open Constrexpr
+open Constrexpr_ops
 open Topconstr
+open Notation_term
+open Notation_ops
 open Prettyp
 open Search
 
 open Evar_refiner
+open Goal
 open Logic
 open Pfedit
+open Proof
+open Proof_using
+open Proof_global
 open Proof_type
 open Redexpr
 open Refiner
 open Tacmach
-open Decl_proof_instr
 open Tactic_debug
+
+open Decl_proof_instr
 open Decl_mode
 
 open Auto
@@ -129,11 +156,11 @@ open Equality
 open Evar_tactics
 open Extraargs
 open Extratactics
-open Hiddentac
 open Hipattern
 open Inv
 open Leminv
-open Refine
+open Tacsubst
+open Tacintern
 open Tacinterp
 open Tacticals
 open Tactics
@@ -145,7 +172,6 @@ open Command
 open Indschemes
 open Ind_tables
 open Auto_ind_decl
-open Lemmas
 open Coqinit
 open Coqtop
 open Discharge
@@ -153,7 +179,7 @@ open Himsg
 open Metasyntax
 open Mltop
 open Record
-open Toplevel
+open Coqloop
 open Vernacentries
 open Vernacinterp
 open Vernac
@@ -171,22 +197,22 @@ let parse_vernac = Pcoq.parse_string Pcoq.Vernac_.vernac;;
 (* build a term of type glob_constr without type-checking or resolution of 
    implicit syntax *)
 
-let e s =
-  Constrintern.intern_constr Evd.empty (Global.env()) (parse_constr s);;
+let e s = Constrintern.intern_constr (Global.env()) (parse_constr s);;
 
 (* build a term of type constr with type-checking and resolution of 
    implicit syntax *)
 
 let constr_of_string s = 
-  Constrintern.interp_constr Evd.empty (Global.env()) (parse_constr s);;
+  Constrintern.interp_constr (Global.env()) Evd.empty (parse_constr s);;
 
 (* get the body of a constant *)
 
 open Declarations;;
+open Declareops;;
 
 let constbody_of_string s =
   let b = Global.lookup_constant (Nametab.locate_constant (qualid_of_string s)) in
-  Option.get (body_of_constant b);;
+  Option.get (Declareops.body_of_constant Opaqueproof.empty_opaquetab b);;
 
 (* Get the current goal *)
 (*
@@ -196,14 +222,15 @@ let get_nth_goal n = nth_goal_of_pftreestate n (Pfedit.get_pftreestate ());;
 let current_goal () = get_nth_goal 1;;
 *)
 let pf_e gl s = 
-  Constrintern.interp_constr (project gl) (pf_env gl) (parse_constr s);;
+  Constrintern.interp_constr (pf_env gl) (project gl) (parse_constr s);;
 
 (* Set usual printing since the global env is available from the tracer *)
-let _ = Constrextern.in_debugger := false
+let _ = Flags.in_debugger := false
+let _ = Flags.in_toplevel := true
 let _ = Constrextern.set_extern_reference
   (fun loc _ r -> Libnames.Qualid (loc,Nametab.shortest_qualid_of_global Idset.empty r));;
 
-open Toplevel
+open Coqloop
 let go = loop
 
 let _ =
diff --git a/dev/db b/dev/db
index 63c98bb6..f259b50e 100644
--- a/dev/db
+++ b/dev/db
@@ -1,20 +1,28 @@
 load_printer "gramlib.cma"
+load_printer "str.cma"
 load_printer "printers.cma"
 
+install_printer Top_printers.ppfuture
+
 install_printer Top_printers.ppid
 install_printer Top_printers.ppidset
+install_printer Top_printers.ppevar
 install_printer Top_printers.ppevarsubst
+install_printer Top_printers.ppexistentialfilter
+install_printer Top_printers.ppexistentialset
 install_printer Top_printers.ppintset
 install_printer Top_printers.pplab
 install_printer Top_printers.ppdir
 install_printer Top_printers.ppmp
 install_printer Top_printers.ppkn
 install_printer Top_printers.ppcon
+install_printer Top_printers.ppwf_paths
 install_printer Top_printers.ppmind
 install_printer Top_printers.ppsp
 install_printer Top_printers.ppqualid
 install_printer Top_printers.ppclindex
 install_printer Top_printers.ppbigint
+install_printer Top_printers.pp_transparent_state
 
 install_printer Top_printers.pppattern
 install_printer Top_printers.ppglob_constr
@@ -26,10 +34,16 @@ install_printer Top_printers.ppconstraints
 install_printer Top_printers.pptype
 install_printer Top_printers.ppj
 install_printer Top_printers.ppenv
+install_printer Top_printers.ppnamedcontextval
+install_printer Top_printers.pp_stack_t
+install_printer Top_printers.pp_cst_stack_t
 
 install_printer Top_printers.ppmetas
 install_printer Top_printers.ppevm
+install_printer Top_printers.ppgoalgoal
 install_printer Top_printers.ppgoal
+install_printer Top_printers.ppproofview
+install_printer Top_printers.pphintdb
 
 install_printer Top_printers.pptac
 install_printer Top_printers.ppobj
@@ -37,3 +51,10 @@ install_printer Top_printers.pploc
 install_printer Top_printers.prsubst
 install_printer Top_printers.prdelta
 install_printer Top_printers.ppfconstr
+install_printer Top_printers.ppgenarginfo
+install_printer Top_printers.ppist
+install_printer Top_printers.ppconstrunderbindersidmap
+install_printer Top_printers.ppunbound_ltac_var_map
+install_printer Top_printers.ppididmap
+install_printer Top_printers.ppclosure
+install_printer Top_printers.ppclosedglobconstr
diff --git a/dev/db_printers.ml b/dev/db_printers.ml
index f535de4a..e843bbc5 100644
--- a/dev/db_printers.ml
+++ b/dev/db_printers.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -10,7 +10,7 @@ open Names
 
 let pp s = pp (hov 0 s)
 
-let prid id = Format.print_string (string_of_id id)
-let prsp sp = Format.print_string (string_of_path sp)
+let prid id = Format.print_string (Id.to_string id)
+let prsp sp = Format.print_string (DirPath.to_string sp)
 
 
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)\\
diff --git a/dev/dynlink.ml b/dev/dynlink.ml
new file mode 100644
index 00000000..810e0ffc
--- /dev/null
+++ b/dev/dynlink.ml
@@ -0,0 +1,51 @@
+
+(** Some architectures may have a native ocaml compiler but no native
+    dynlink.cmxa (e.g. ARM). If you still want to build a native coqtop
+    there, you'll need this dummy implementation of Dynlink.
+    Compile it and install with:
+
+      ocamlopt -a -o dynlink.cmxa dynlink.ml
+      sudo cp -i dynlink.cmxa `ocamlopt -where`
+
+    Then build coq this way: ./configure -natdynlink no && make world
+*)
+
+let is_native = true (* This file will only be given to the native compiler *)
+
+type linking_error =
+| Undefined_global of string
+| Unavailable_primitive of string
+| Uninitialized_global of string
+
+type error =
+| Not_a_bytecode_file of string
+| Inconsistent_import of string
+| Unavailable_unit of string
+| Unsafe_file
+| Linking_error of string * linking_error
+| Corrupted_interface of string
+| File_not_found of string
+| Cannot_open_dll of string
+| Inconsistent_implementation of string
+
+exception Error of error
+
+let error_message = function
+  | Not_a_bytecode_file s -> "Native dynamic link not supported (module "^s^")"
+  | _ -> "Native dynamic link not supported"
+
+let loadfile : string -> unit = fun s -> raise (Error (Not_a_bytecode_file s))
+let loadfile_private = loadfile
+
+let adapt_filename s = s
+
+let init () = ()
+let allow_only : string list -> unit = fun _ -> ()
+let prohibit : string list -> unit = fun _ -> ()
+let default_available_units : unit -> unit = fun _ -> ()
+let allow_unsafe_modules : bool -> unit = fun _ -> ()
+let add_interfaces : string list -> string list -> unit = fun _ _ -> ()
+let add_available_units : (string * Digest.t) list -> unit = fun _ -> ()
+let clear_available_units : unit -> unit = fun _ -> ()
+let digest_interface : string -> string list -> Digest.t =
+ fun _ _ -> failwith "digest_interface"
diff --git a/dev/header b/dev/header
index 4dd8f5a9..e5184df3 100644
--- a/dev/header
+++ b/dev/header
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/dev/include b/dev/include
index 69ac3c41..b2eb280d 100644
--- a/dev/include
+++ b/dev/include
@@ -10,8 +10,9 @@
    Alternatively, you can avoid typing #use "include" after each Drop
    by adding the following lines in your $HOME/.ocamlinit :
 
+   #directory "+compiler-libs";;
    if Filename.basename Sys.argv.(0) = "coqtop.byte"
-   then ignore (Toploop.use_silently Format.std_formatter "include")
+   then ignore (Toploop.use_silently Format.std_formatter "dev/include")
 *)
 
 (* For OCaml 3.10.x:
@@ -28,25 +29,50 @@
 
 #install_printer  (* pattern *) pppattern;;
 #install_printer  (* glob_constr *) ppglob_constr;;
-
+#install_printer  (* open constr *) ppopenconstr;;
 #install_printer  (* constr *) ppconstr;;
 #install_printer  (* constr_substituted *) ppsconstr;; 
+#install_printer  (* constraints *)  ppconstraints;;
+#install_printer  (* univ constraints *)  ppuniverseconstraints;;
 #install_printer  (* universe *)  ppuni;;
+#install_printer  (* universes *)  ppuniverse;;
 #install_printer  (* universes *)  ppuniverses;;
+#install_printer  (* univ level *) ppuni_level;;
+#install_printer  (* univ context *) ppuniverse_context;;
+#install_printer  (* univ context future *) ppuniverse_context_future;;
+#install_printer  (* univ context set *) ppuniverse_context_set;;
+#install_printer  (* univ set *) ppuniverse_set;;
+#install_printer  (* univ instance *) ppuniverse_instance;;
+#install_printer  (* univ subst *) ppuniverse_subst;;
+#install_printer  (* univ full subst *) ppuniverse_level_subst;;
+#install_printer  (* univ opt subst *) ppuniverse_opt_subst;;
+#install_printer  (* evar univ ctx *) ppevar_universe_context;;
+#install_printer  (* constraints_map *) ppconstraints_map;;
+#install_printer  (* inductive *) ppind;;
+#install_printer  (* 'a scheme_kind *) ppscheme;;
 #install_printer  (* type_judgement *) pptype;;
 #install_printer  (* judgement *) ppj;;
+#install_printer  (* id set *) ppidset;;
+#install_printer  (* int set *) ppintset;;
+
+#install_printer  (* Reductionops stcak of unfolded constants *) pp_cst_stack_t;;
+#install_printer  (* Reductionops machine stack *) pp_stack_t;;
 
-#install_printer  (* hint_db *)  print_hint_db;;
+(*#install_printer  (* hint_db *)  print_hint_db;;*)
 (*#install_printer  (* hints_path *)  pphintspath;;*)
 #install_printer  (* goal *)  ppgoal;;
 (*#install_printer  (* sigma goal *)  ppsigmagoal;;*)
 (*#install_printer  (* proof *)  pproof;;*)
 #install_printer  (* Goal.goal *)  ppgoalgoal;;
+#install_printer  (* proofview *)  ppproofview;;
 #install_printer  (* metaset.t *) ppmetas;;
+#install_printer  (* evar *)  ppevar;;
 #install_printer  (* evar_map *)  ppevm;;
-#install_printer  (* ExistentialSet.t *) ppexistentialset;;
+#install_printer  (* Evar.Set.t *) ppexistentialset;;
 #install_printer  (* clenv *) ppclenv;;
 #install_printer  (* env *) ppenv;;
+#install_printer  (* Hint_db.t *) pphintdb;;
+#install_printer  (* named_context_val *) ppnamedcontextval;;
 
 #install_printer  (* tactic *) pptac;;
 #install_printer  (* object *) ppobj;;
@@ -54,3 +80,5 @@
 #install_printer  (* generic_argument *) pp_generic_argument;;
 
 #install_printer  (* fconstr *) ppfconstr;;
+
+#install_printer (* Future.computation *) ppfuture;;
diff --git a/dev/make-installer-win32.sh b/dev/make-installer-win32.sh
new file mode 100755
index 00000000..ec7cd577
--- /dev/null
+++ b/dev/make-installer-win32.sh
@@ -0,0 +1,20 @@
+#!/bin/sh
+
+NSIS="$BASE/NSIS/makensis"
+ZIP=_make.zip
+URL1=http://sourceforge.net/projects/gnuwin32/files/make/3.81/make-3.81-bin.zip/download
+URL2=http://sourceforge.net/projects/gnuwin32/files/make/3.81/make-3.81-dep.zip/download
+
+[ -e config/Makefile ] || ./configure -prefix ./ -with-doc no
+make -j2 
+if [ ! -e bin/make.exe ]; then
+  wget -O $ZIP $URL1 && 7z x $ZIP "bin/*"
+  wget -O $ZIP $URL2 && 7z x $ZIP "bin/*"
+  rm -rf $ZIP
+fi
+VERSION=`grep ^VERSION= config/Makefile | cut -d = -f 2`
+cd dev/nsis
+"$NSIS" -DVERSION=$VERSION -DGTK_RUNTIME="`cygpath -w $BASE`" coq.nsi
+echo Installer:
+ls -h $PWD/*exe
+cd ../..
diff --git a/dev/make-sdk-win32.sh b/dev/make-sdk-win32.sh
new file mode 100755
index 00000000..0112324d
--- /dev/null
+++ b/dev/make-sdk-win32.sh
@@ -0,0 +1,370 @@
+#!/bin/bash
+
+# To run this script install cygwin by running setup-x86.exe from cygwin.com
+# Install the standard packages plus wget.  Then run this script.
+
+# Sworn by Enrico Tassi <enrico.tassi@inra.fr>
+# Modified to support other directories and almost support spaces in paths
+# by Jason Gross <jgross@mit.edu>
+# License: Expat/MIT http://opensource.org/licenses/MIT
+
+# This script reads the following environment variables:
+# VERBOSE     - set to non-empty to have wget/this script be more verbose, for debugging purposes
+# BASE        - set to non-empty to give a different location for the zip file, e.g., if /cygdrive/c is full or doesn't exist
+
+set -e
+if [ ! -z "$VERBOSE" ]
+then
+  set -x
+fi
+
+# Resources
+ocaml=ocaml-4.01.0-i686-mingw64-installer3.exe
+glib=base-windows-0.18.1.1.13.356@BUILD_ec06e9.txz
+gtk=base-gtk-2.24.18.1.58@BUILD_594ca8.txz
+lablgtk=lablgtk-2.18.0.tar.gz
+camlp5=camlp5-6.11.tgz
+nsis=nsis-2.46-setup.exe
+
+ocaml_URL='http://yquem.inria.fr/~protzenk/caml-installer/'$ocaml
+lablgtk_URL='https://forge.ocamlcore.org/frs/download.php/1261/'$lablgtk
+glib_URL='http://dl.arirux.de/5/binaries32/'$glib
+gtk_URL='http://dl.arirux.de/5/binaries32/'$gtk
+camlp5_URL='http://pauillac.inria.fr/~ddr/camlp5/distrib/src/'$camlp5
+nsis_URL='http://netcologne.dl.sourceforge.net/project/nsis/NSIS%202/2.46/'$nsis
+
+cygwin=setup-${HOSTTYPE/i6/x}.exe
+cygwin_URL='http://cygwin.com/'$cygwin
+cygwin_PKGS=p7zip,zip,sed,make,mingw64-i686-gcc-g++,mingw64-i686-gcc-core,mingw64-i686-gcc,patch,rlwrap,libreadline6,diffutils
+
+has_spaces() {
+    test -z "$2"
+}
+# utilities
+# http://www.dependencywalker.com/depends22_x86.zip
+
+# The SDK itself
+REVISION=85-1
+# support for working on computers that don't have a C: drive
+if [ -z "$BASE" ]
+then
+  TRUE_BASE=/cygdrive/c
+else
+  # get absolute path
+  TRUE_BASE="$(readlink -f "$BASE")"
+fi
+BASE="$TRUE_BASE/CoqSDK-$REVISION"
+
+if [ -z "$VERBOSE" ]
+then
+  WGET_ARGS="-N -q"
+else
+  WGET_ARGS="-N"
+fi
+
+# Windows has a version of FIND in C:/Windows/system32/find, and we don't want to use that
+if [ -x /usr/bin/find ]
+then
+  FIND=/usr/bin/find
+else
+  echo "WARNING: /usr/bin/find does not exist.  Falling back on:"
+  which find
+  FIND=find
+fi
+
+WGET_ARGS="-N -q"
+
+if [ "$(has_spaces $BASE; echo $?)" -ne 0 ]; then
+  echo "ERROR: The current base directory ($BASE) has spaces."
+  echo "ERROR: building lablgtk would fail."
+  exit 1
+fi
+
+cyg_install() {
+  if [ ! -e "$cygwin" ]; then wget $WGET_ARGS "$cygwin_URL"; fi
+  chmod a+x "$cygwin"
+  cygstart -w "$cygwin" -q -P $@
+}
+
+sanity_check() {
+  echo "Check: wget."
+  (which wget) || \
+	  (echo "Please install wget using the cygwin installer and retry.";\
+	   exit 1)
+  echo "Check: 7z, gcc.  If it fails wait for cygwin to complete and retry"
+  (which 7z && which i686-w64-mingw32-gcc) || \
+	  (echo "Some cygwin package is not installed.";\
+	   echo "Please wait for cygwin to finish and retry.";\
+	   cyg_install $cygwin_PKGS;\
+	   exit 1)
+}
+
+install_base() {
+  echo "Setting up $BASE"
+  rm -rf "$BASE"
+  mkdir -p "$BASE"
+}
+
+make_environ() {
+  echo "Setting up $BASE/environ"
+  pushd "$BASE" >/dev/null
+  cat > environ <<- EOF
+	cyg_install() {
+	  if [ ! -e "$cygwin" ]; then wget $WGET_ARGS "$cygwin_URL"; fi
+	  chmod a+x "$cygwin"
+	  cygstart -w "$cygwin" -q -P \$@
+	}
+	# Sanity checks: is the mingw64-i686-gcc package installed?
+	(which i686-w64-mingw32-gcc && which make && which sed) || \\
+		(echo "Some cygwin package is not installed.";\\
+	         echo "Please wait for cygwin to finish and retry.";\\
+	 	 cyg_install $cygwin_PKGS;\\
+		 exit 1) || exit 1
+
+	export BASE="\$( cd "\$( dirname "\${BASH_SOURCE[0]}" )" && pwd )"
+	export PATH="\$BASE/bin:\$PATH"
+	export OCAMLLIB="\$(cygpath -m "\$BASE")/lib"
+	export OCAMLFIND_CONF="\$(cygpath -m "\$BASE")/etc/findlib.conf"
+	sed s"|@BASE@|\$(cygpath -m "\$BASE")|g" "\$BASE/lib/ld.conf.in" \\
+	        > "\$BASE/lib/ld.conf"
+	sed s"|@BASE@|\$(cygpath -m "\$BASE")|g" "\$BASE/lib/topfind.in" \\
+	        > "\$BASE/lib/topfind"
+	sed s"|@BASE@|\$(cygpath -m "\$BASE")|g" "\$BASE/etc/findlib.conf.in" \\
+	        > "\$BASE/etc/findlib.conf"
+	echo "Good.  You can now build Coq and Coqide from cygwin."
+	EOF
+  popd >/dev/null
+}
+
+download() {
+  echo "Downloading some software:"
+  if [ ! -e "$ocaml" ]; then
+    echo "- downloading OCaml..."
+    wget $WGET_ARGS "$ocaml_URL"
+  fi
+  chmod a+x "$ocaml"
+  if [ ! -e "$lablgtk" ]; then
+    echo "- downloading lablgtk..."
+    wget $WGET_ARGS --no-check-certificate "$lablgtk_URL"
+  fi
+  if [ ! -e "$gtk" ]; then
+    echo "- downloading gtk..."
+    wget $WGET_ARGS "$gtk_URL"
+  fi
+  if [ ! -e "$glib" ]; then
+    echo "- downloading glib..."
+    wget $WGET_ARGS "$glib_URL"
+  fi
+  if [ ! -e "$camlp5" ]; then
+    echo "- downloading camlp5..."
+    wget $WGET_ARGS "$camlp5_URL"
+  fi
+  if [ ! -e "$nsis" ]; then
+    echo "- downloading nsis..."
+    wget $WGET_ARGS "$nsis_URL"
+  fi
+}
+
+cleanup() {
+  rm -rf tmp build
+}
+
+install_gtk() {
+  echo "Installing $glib"
+  tar -xJf "$glib" -C "$BASE"
+  echo "Installing $gtk"
+  tar -xJf "$gtk" -C "$BASE"
+}
+
+install_ocaml() {
+  echo "Installing $ocaml"
+  mkdir -p tmp
+  7z -otmp x "$ocaml" >/dev/null
+  cp -r tmp/\$_OUTDIR/bin "$BASE/"
+  cp -r tmp/bin "$BASE/"
+  cp -r tmp/\$_OUTDIR/lib "$BASE/"
+  cp -r tmp/lib "$BASE/"
+  cp -r tmp/\$_OUTDIR/etc "$BASE/"
+  "$FIND" "$BASE" -name '*.dll' -o -name '*.exe' | tr '\n' '\0' \
+	  | xargs -0 chmod a+x
+  mv "$BASE/lib/topfind" "$BASE/lib/topfind.in"
+  sed -i 's|@SITELIB@|@BASE@/lib/site-lib|g' "$BASE/lib/topfind.in"
+  cat > "$BASE/lib/ld.conf.in" <<- EOF
+	@BASE@/lib
+	@BASE@/lib/stublibs
+	EOF
+  cat > "$BASE/etc/findlib.conf.in" <<- EOF
+	destdir="@BASE@/lib/site-lib"
+	path="@BASE@/lib/site-lib"
+	stdlib="@BASE@/lib"
+	ldconf="@BASE@/lib/ld.conf"
+	ocamlc="ocamlc.opt"
+	ocamlopt="ocamlopt.opt"
+	ocamldep="ocamldep.opt"
+	ocamldoc="ocamldoc.opt"
+	EOF
+  cp "$BASE/lib/topdirs.cmi" "$BASE/lib/compiler-libs/"
+}
+
+build_install_lablgtk() {
+  echo "Building $lablgtk"
+  mkdir -p build
+  tar -xzf "$lablgtk" -C build
+  cd build/lablgtk-*
+  patch -p1 <<EOT
+--- lablgtk-2.18.0/src/glib.mli	2013-10-01 01:31:50.000000000 -0700
++++ lablgtk-2.18.0.new/src/glib.mli	2013-12-06 11:57:34.203675200 -0800
+@@ -75,6 +75,7 @@
+   type condition = [ \`ERR | \`HUP | \`IN | \`NVAL | \`OUT | \`PRI]
+   type id
+   val channel_of_descr : Unix.file_descr -> channel
++  val channel_of_descr_socket : Unix.file_descr -> channel
+   val add_watch :
+     cond:condition list -> callback:(condition list -> bool) -> ?prio:int -> channel -> id
+   val remove : id -> unit
+--- lablgtk-2.18.0/src/glib.ml	2013-10-01 01:31:50.000000000 -0700
++++ lablgtk-2.18.0.new/src/glib.ml	2013-12-06 11:57:53.070804800 -0800
+@@ -72,6 +72,8 @@
+   type id
+   external channel_of_descr : Unix.file_descr -> channel
+     = "ml_g_io_channel_unix_new"
++  external channel_of_descr_socket : Unix.file_descr -> channel
++    = "ml_g_io_channel_unix_new_socket"
+   external remove : id -> unit = "ml_g_source_remove"
+   external add_watch :
+     cond:condition list -> callback:(condition list -> bool) -> ?prio:int -> channel -> id
+--- lablgtk-2.18.0/src/ml_glib.c	2013-10-01 01:31:50.000000000 -0700
++++ lablgtk-2.18.0.new/src/ml_glib.c	2013-12-10 02:03:33.940371800 -0800
+@@ -25,6 +25,8 @@
+ #include <string.h>
+ #include <locale.h>
+ #ifdef _WIN32
++/* to kill a #warning: include winsock2.h before windows.h */
++#include <winsock2.h>
+ #include "win32.h"
+ #include <wtypes.h>
+ #include <io.h>
+@@ -38,6 +40,11 @@
+ #include <caml/callback.h>
+ #include <caml/threads.h>
+
++#ifdef _WIN32
++/* for Socket_val */
++#include <caml/unixsupport.h>
++#endif
++
+ #include "wrappers.h"
+ #include "ml_glib.h"
+ #include "glib_tags.h"
+@@ -325,14 +332,23 @@
+
+ #ifndef _WIN32
+ ML_1 (g_io_channel_unix_new, Int_val, Val_GIOChannel_noref)
++CAMLprim value ml_g_io_channel_unix_new_socket (value arg1) {
++  return Val_GIOChannel_noref (g_io_channel_unix_new (Int_val (arg1)));
++}
+
+ #else
+ CAMLprim value ml_g_io_channel_unix_new(value wh)
+ {
+   return Val_GIOChannel_noref
+-    (g_io_channel_unix_new
++    (g_io_channel_win32_new_fd
+      (_open_osfhandle((long)*(HANDLE*)Data_custom_val(wh), O_BINARY)));
+ }
++
++CAMLprim value ml_g_io_channel_unix_new_socket(value wh)
++{
++  return Val_GIOChannel_noref
++    (g_io_channel_win32_new_socket(Socket_val(wh)));
++}
+ #endif
+
+ static gboolean ml_g_io_channel_watch(GIOChannel *s, GIOCondition c,
+EOT
+  #sed -i s'/$PKG_CONFIG/"$PKG_CONFIG"/g' configure
+  #sed -i s'/""$PKG_CONFIG""/"$PKG_CONFIG"/g' configure
+  ./configure --disable-gtktest --prefix="$(cygpath -m "$BASE")" \
+	  >log-configure 2>&1
+  sed -i 's?\\?/?g' config.make
+  make >log-make 2>&1
+  make opt >>log-make 2>&1
+  #echo "Testing $lablgtk"
+  #cd src
+  #./lablgtk2 ../examples/calc.ml
+  #./lablgtk2 -all ../examples/calc.ml
+  #cd ..
+  echo "Installing $lablgtk"
+  make install >>log-make 2>&1
+  cd ../..
+}
+
+build_install_camlp5() {
+  echo "Building $camlp5"
+  mkdir -p build
+  tar -xzf "$camlp5" -C build
+  cd build/camlp5-*
+  ./configure >log-configure 2>&1
+  sed -i 's/EXT_OBJ=.obj/EXT_OBJ=.o/' config/Makefile
+  sed -i 's/EXT_LIB=.lib/EXT_LIB=.a/' config/Makefile
+  make world.opt >log-make 2>&1
+  echo "Installing $camlp5"
+  make install >>log-make 2>&1
+  cd ../..
+}
+
+install_nsis() {
+  echo "Installing $nsis"
+  rm -rf tmp
+  mkdir -p tmp
+  7z -otmp x $nsis >/dev/null
+  mkdir "$BASE/NSIS"
+  cp -r tmp/\$_OUTDIR/* "$BASE/NSIS"
+  rm -rf tmp/\$_OUTDIR
+  rm -rf tmp/\$PLUGINSDIR
+  cp -r tmp/* "$BASE/NSIS"
+}
+
+zip_sdk() {
+  echo "Generating CoqSDK-${REVISION}.zip"
+  here="`pwd`"
+  cd "$BASE/.."
+  rm -f "$here/CoqSDK-${REVISION}.zip"
+  zip -q -r "$here/CoqSDK-${REVISION}.zip" "$(basename "$BASE")"
+  cd "$here"
+}
+
+diet_sdk() {
+  rm -rf "$BASE"/+*
+  rm -rf "$BASE"/bin/camlp4*
+  rm -rf "$BASE"/lib/camlp4/
+  rm -rf "$BASE"/lib/site-lib/camlp4/
+}
+
+victory(){
+  echo "Output file: CoqSDK-${REVISION}.zip "\
+	  "(`du -sh CoqSDK-${REVISION}.zip | cut -f 1`)"
+  echo "Usage: unpack and source the environ file at its root"
+}
+
+if [ -z "$1" ]; then
+  sanity_check
+  download
+  cleanup
+  install_base
+  install_nsis
+  install_ocaml
+  install_gtk
+  make_environ
+  . "$BASE/environ"
+  build_install_lablgtk
+  build_install_camlp5
+  diet_sdk
+  make_environ
+  zip_sdk
+  cleanup
+  victory
+else
+  # just one step
+  $1
+fi
diff --git a/dev/nsis/FileAssociation.nsh b/dev/nsis/FileAssociation.nsh
new file mode 100644
index 00000000..b8c1e5ee
--- /dev/null
+++ b/dev/nsis/FileAssociation.nsh
@@ -0,0 +1,190 @@
+/*
+_____________________________________________________________________________
+ 
+                       File Association
+_____________________________________________________________________________
+ 
+ Based on code taken from http://nsis.sourceforge.net/File_Association 
+ 
+ Usage in script:
+ 1. !include "FileAssociation.nsh"
+ 2. [Section|Function]
+      ${FileAssociationFunction} "Param1" "Param2" "..." $var
+    [SectionEnd|FunctionEnd]
+ 
+ FileAssociationFunction=[RegisterExtension|UnRegisterExtension]
+ 
+_____________________________________________________________________________
+ 
+ ${RegisterExtension} "[executable]" "[extension]" "[description]"
+ 
+"[executable]"     ; executable which opens the file format
+                   ;
+"[extension]"      ; extension, which represents the file format to open
+                   ;
+"[description]"    ; description for the extension. This will be display in Windows Explorer.
+                   ;
+ 
+ 
+ ${UnRegisterExtension} "[extension]" "[description]"
+ 
+"[extension]"      ; extension, which represents the file format to open
+                   ;
+"[description]"    ; description for the extension. This will be display in Windows Explorer.
+                   ;
+ 
+_____________________________________________________________________________
+ 
+                         Macros
+_____________________________________________________________________________
+ 
+ Change log window verbosity (default: 3=no script)
+ 
+ Example:
+ !include "FileAssociation.nsh"
+ !insertmacro RegisterExtension
+ ${FileAssociation_VERBOSE} 4   # all verbosity
+ !insertmacro UnRegisterExtension
+ ${FileAssociation_VERBOSE} 3   # no script
+*/
+ 
+ 
+!ifndef FileAssociation_INCLUDED
+!define FileAssociation_INCLUDED
+ 
+!include Util.nsh
+ 
+!verbose push
+!verbose 3
+!ifndef _FileAssociation_VERBOSE
+  !define _FileAssociation_VERBOSE 3
+!endif
+!verbose ${_FileAssociation_VERBOSE}
+!define FileAssociation_VERBOSE `!insertmacro FileAssociation_VERBOSE`
+!verbose pop
+ 
+!macro FileAssociation_VERBOSE _VERBOSE
+  !verbose push
+  !verbose 3
+  !undef _FileAssociation_VERBOSE
+  !define _FileAssociation_VERBOSE ${_VERBOSE}
+  !verbose pop
+!macroend
+ 
+ 
+ 
+!macro RegisterExtensionCall _EXECUTABLE _EXTENSION _DESCRIPTION
+  !verbose push
+  !verbose ${_FileAssociation_VERBOSE}
+  Push `${_DESCRIPTION}`
+  Push `${_EXTENSION}`
+  Push `${_EXECUTABLE}`
+  ${CallArtificialFunction} RegisterExtension_
+  !verbose pop
+!macroend
+ 
+!macro UnRegisterExtensionCall _EXTENSION _DESCRIPTION
+  !verbose push
+  !verbose ${_FileAssociation_VERBOSE}
+  Push `${_EXTENSION}`
+  Push `${_DESCRIPTION}`
+  ${CallArtificialFunction} UnRegisterExtension_
+  !verbose pop
+!macroend
+ 
+ 
+ 
+!define RegisterExtension `!insertmacro RegisterExtensionCall`
+!define un.RegisterExtension `!insertmacro RegisterExtensionCall`
+ 
+!macro RegisterExtension
+!macroend
+ 
+!macro un.RegisterExtension
+!macroend
+ 
+!macro RegisterExtension_
+  !verbose push
+  !verbose ${_FileAssociation_VERBOSE}
+ 
+  Exch $R2 ;exe
+  Exch
+  Exch $R1 ;ext
+  Exch
+  Exch 2
+  Exch $R0 ;desc
+  Exch 2
+  Push $0
+  Push $1
+ 
+  ReadRegStr $1 HKCR $R1 ""  ; read current file association
+  StrCmp "$1" "" NoBackup  ; is it empty
+  StrCmp "$1" "$R0" NoBackup  ; is it our own
+    WriteRegStr HKCR $R1 "backup_val" "$1"  ; backup current value
+NoBackup:
+  WriteRegStr HKCR $R1 "" "$R0"  ; set our file association
+ 
+  ReadRegStr $0 HKCR $R0 ""
+  StrCmp $0 "" 0 Skip
+    WriteRegStr HKCR "$R0" "" "$R0"
+    WriteRegStr HKCR "$R0\shell" "" "open"
+    WriteRegStr HKCR "$R0\DefaultIcon" "" "$R2,0"
+Skip:
+  WriteRegStr HKCR "$R0\shell\open\command" "" '"$R2" "%1"'
+  WriteRegStr HKCR "$R0\shell\edit" "" "Edit $R0"
+  WriteRegStr HKCR "$R0\shell\edit\command" "" '"$R2" "%1"'
+ 
+  Pop $1
+  Pop $0
+  Pop $R2
+  Pop $R1
+  Pop $R0
+ 
+  !verbose pop
+!macroend
+ 
+ 
+ 
+!define UnRegisterExtension `!insertmacro UnRegisterExtensionCall`
+!define un.UnRegisterExtension `!insertmacro UnRegisterExtensionCall`
+ 
+!macro UnRegisterExtension
+!macroend
+ 
+!macro un.UnRegisterExtension
+!macroend
+ 
+!macro UnRegisterExtension_
+  !verbose push
+  !verbose ${_FileAssociation_VERBOSE}
+ 
+  Exch $R1 ;desc
+  Exch
+  Exch $R0 ;ext
+  Exch
+  Push $0
+  Push $1
+ 
+  ReadRegStr $1 HKCR $R0 ""
+  StrCmp $1 $R1 0 NoOwn ; only do this if we own it
+  ReadRegStr $1 HKCR $R0 "backup_val"
+  StrCmp $1 "" 0 Restore ; if backup="" then delete the whole key
+  DeleteRegKey HKCR $R0
+  Goto NoOwn
+ 
+Restore:
+  WriteRegStr HKCR $R0 "" $1
+  DeleteRegValue HKCR $R0 "backup_val"
+  DeleteRegKey HKCR $R1 ;Delete key with association name settings
+ 
+NoOwn:
+ 
+  Pop $1
+  Pop $0
+  Pop $R1
+  Pop $R0
+ 
+  !verbose pop
+!macroend
+ 
+!endif # !FileAssociation_INCLUDED
\ No newline at end of file
diff --git a/dev/nsis/coq.nsi b/dev/nsis/coq.nsi
new file mode 100755
index 00000000..90e3fdaa
--- /dev/null
+++ b/dev/nsis/coq.nsi
@@ -0,0 +1,231 @@
+; This script is used to build the Windows install program for Coq.
+
+;NSIS Modern User Interface
+;Written by Joost Verburg
+;Modified by Julien Narboux and Pierre Letouzey and Enrico Tassi
+
+;SetCompress off
+SetCompressor lzma
+; Comment out after debuging.
+
+; The VERSION should be passed as an argument at compile time using :
+;
+
+!define MY_PRODUCT "Coq" ;Define your own software name here
+!define COQ_SRC_PATH "..\.."
+!define OUTFILE "coq-installer-${VERSION}.exe"
+
+!include "MUI2.nsh"
+!include "FileAssociation.nsh"
+
+;--------------------------------
+;Configuration
+
+  Name "Coq"
+
+  ;General
+  OutFile "${OUTFILE}"
+
+  ;Folder selection page
+  InstallDir "C:\${MY_PRODUCT}"
+  
+  ;Remember install folder
+  InstallDirRegKey HKCU "Software\${MY_PRODUCT}" ""
+
+;--------------------------------
+;Modern UI Configuration
+
+  !insertmacro MUI_PAGE_WELCOME
+  !insertmacro MUI_PAGE_LICENSE "${COQ_SRC_PATH}/LICENSE"
+  !insertmacro MUI_PAGE_COMPONENTS
+  !define MUI_DIRECTORYPAGE_TEXT_TOP "Select where to install Coq.  The path MUST NOT include spaces."
+  !insertmacro MUI_PAGE_DIRECTORY
+  !insertmacro MUI_PAGE_INSTFILES
+  !insertmacro MUI_PAGE_FINISH
+  
+  !insertmacro MUI_UNPAGE_WELCOME
+  !insertmacro MUI_UNPAGE_CONFIRM
+  !insertmacro MUI_UNPAGE_INSTFILES
+  !insertmacro MUI_UNPAGE_FINISH  
+
+;--------------------------------
+;Languages
+ 
+  !insertmacro MUI_LANGUAGE "English"
+  
+;--------------------------------
+;Language Strings
+
+  ;Description
+  LangString DESC_1 ${LANG_ENGLISH} "This package contains Coq and CoqIDE."
+  LangString DESC_2 ${LANG_ENGLISH} "This package contains the development files needed in order to build a plugin for Coq."
+
+;--------------------------------
+; Check for white spaces
+Function .onVerifyInstDir
+  StrLen $0 "$INSTDIR"
+  StrCpy $1 0
+  ${While} $1 < $0
+    StrCpy $3 $INSTDIR 1 $1
+    StrCmp $3 " " SpacesInPath
+    IntOp $1 $1 + 1
+  ${EndWhile}
+  Goto done
+  SpacesInPath:
+  Abort
+  done:
+FunctionEnd
+
+;--------------------------------
+;Installer Sections
+
+
+Section "Coq" Sec1
+
+  SetOutPath "$INSTDIR\"
+
+  SetOutPath "$INSTDIR\bin"
+  File ${COQ_SRC_PATH}\bin\*.exe
+  ; make.exe and its dll
+  File ${COQ_SRC_PATH}\bin\make.exe
+  File ${COQ_SRC_PATH}\bin\libiconv2.dll
+  File ${COQ_SRC_PATH}\bin\libintl3.dll
+
+  SetOutPath "$INSTDIR\lib\theories"
+  File /r ${COQ_SRC_PATH}\theories\*.vo
+  File /r ${COQ_SRC_PATH}\theories\*.v
+  File /r ${COQ_SRC_PATH}\theories\*.glob
+  File /r ${COQ_SRC_PATH}\theories\*.cmi
+  File /r ${COQ_SRC_PATH}\theories\*.cmxs
+  SetOutPath "$INSTDIR\lib\plugins"
+  File /r ${COQ_SRC_PATH}\plugins\*.vo
+  File /r ${COQ_SRC_PATH}\plugins\*.v
+  File /r ${COQ_SRC_PATH}\plugins\*.glob
+  File /r ${COQ_SRC_PATH}\plugins\*.cmi
+  File /r ${COQ_SRC_PATH}\plugins\*.cmxs
+  SetOutPath "$INSTDIR\lib\tools\coqdoc"
+  File ${COQ_SRC_PATH}\tools\coqdoc\coqdoc.sty
+  File ${COQ_SRC_PATH}\tools\coqdoc\coqdoc.css
+  SetOutPath "$INSTDIR\emacs"
+  File ${COQ_SRC_PATH}\tools\*.el
+  SetOutPath "$INSTDIR\man"
+  File ${COQ_SRC_PATH}\man\*.1
+  SetOutPath "$INSTDIR\lib\toploop"
+  File ${COQ_SRC_PATH}\stm\*top.cmxs
+  File ${COQ_SRC_PATH}\ide\*top.cmxs
+
+  ; CoqIDE
+  SetOutPath "$INSTDIR\ide\"
+  File ${COQ_SRC_PATH}\ide\*.png
+  SetOutPath "$INSTDIR\share\gtksourceview-2.0\language-specs\"
+  File ${COQ_SRC_PATH}\ide\*.lang
+  File ${COQ_SRC_PATH}\ide\*.xml
+
+  ; Start Menu Entries
+  SetOutPath "$INSTDIR"
+  CreateShortCut "$SMPROGRAMS\Coq\CoqIde.lnk" "$INSTDIR\bin\coqide.exe"
+
+  ${registerExtension} "$INSTDIR\bin\coqide.exe" ".v" "Coq Script File"
+
+  SetOutPath "$INSTDIR"
+  File /r ${GTK_RUNTIME}\etc\gtk-2.0
+  SetOutPath "$INSTDIR\bin"
+  File ${GTK_RUNTIME}\bin\*.dll
+  SetOutPath "$INSTDIR\lib"
+  File /r ${GTK_RUNTIME}\lib\gtk-2.0 ${GTK_RUNTIME}\lib\glib-2.0
+  SetOutPath "$INSTDIR\share"
+  File /r ${GTK_RUNTIME}\share\themes
+  File /r ${GTK_RUNTIME}\share\gtksourceview-2.0
+
+  ;Store install folder
+  WriteRegStr HKCU "Software\${MY_PRODUCT}" "" $INSTDIR
+  
+  ;Create uninstaller
+  WriteUninstaller "$INSTDIR\Uninstall.exe"
+  WriteRegStr HKEY_LOCAL_MACHINE "Software\Microsoft\Windows\CurrentVersion\Uninstall\Coq" \
+	  "DisplayName" "Coq Version ${VERSION}"
+  WriteRegStr HKEY_LOCAL_MACHINE "Software\Microsoft\Windows\CurrentVersion\Uninstall\Coq" \
+	  "UninstallString" '"$INSTDIR\Uninstall.exe"'
+
+  WriteRegStr HKEY_LOCAL_MACHINE "Software\Microsoft\Windows\CurrentVersion\Uninstall\Coq" \
+          "DisplayVersion" "${VERSION}"
+
+  WriteRegDWORD HKEY_LOCAL_MACHINE "Software\Microsoft\Windows\CurrentVersion\Uninstall\Coq" \
+          "NoModify" "1"
+  WriteRegDWORD HKEY_LOCAL_MACHINE "Software\Microsoft\Windows\CurrentVersion\Uninstall\Coq" \
+          "NoRepair" "1"
+
+  WriteRegStr HKEY_LOCAL_MACHINE "Software\Microsoft\Windows\CurrentVersion\Uninstall\Coq" \
+          "URLInfoAbout" "http://coq.inria.fr"
+
+; Start Menu Entries
+
+; for the path in the .lnk
+  SetOutPath "$INSTDIR" 
+
+  CreateDirectory "$SMPROGRAMS\Coq"
+  CreateShortCut "$SMPROGRAMS\Coq\Coq.lnk" "$INSTDIR\bin\coqtop.exe"
+  WriteINIStr "$SMPROGRAMS\Coq\The Coq HomePage.url" "InternetShortcut" "URL" "http://coq.inria.fr"
+  WriteINIStr "$SMPROGRAMS\Coq\The Coq Standard Library.url" "InternetShortcut" "URL" "http://coq.inria.fr/library"
+  CreateShortCut "$SMPROGRAMS\Coq\Uninstall.lnk" "$INSTDIR\Uninstall.exe" "" "$INSTDIR\Uninstall.exe" 0
+
+SectionEnd
+
+Section "Coq files for plugin developers" Sec2
+
+  SetOutPath "$INSTDIR\lib\"
+  File /r ${COQ_SRC_PATH}\*.cmxa
+  File /r ${COQ_SRC_PATH}\*.cmi
+  File /r ${COQ_SRC_PATH}\*.cma
+  File /r ${COQ_SRC_PATH}\*.cmo
+  File /r ${COQ_SRC_PATH}\*.a
+  File /r ${COQ_SRC_PATH}\*.o
+
+SectionEnd
+
+;--------------------------------
+;Descriptions
+
+!insertmacro MUI_FUNCTION_DESCRIPTION_BEGIN
+  !insertmacro MUI_DESCRIPTION_TEXT ${Sec1} $(DESC_1)
+  !insertmacro MUI_DESCRIPTION_TEXT ${Sec2} $(DESC_2)
+!insertmacro MUI_FUNCTION_DESCRIPTION_END
+ 
+;--------------------------------
+;Uninstaller Section
+
+Section "Uninstall"
+
+;; We keep the settings 
+;; Delete "$INSTDIR\config\coqide-gtk2rc"
+ 
+  RMDir /r "$INSTDIR\bin"
+  RMDir /r "$INSTDIR\dev"
+  RMDir /r "$INSTDIR\etc"
+  RMDir /r "$INSTDIR\lib"
+  RMDir /r "$INSTDIR\share"
+
+  Delete "$INSTDIR\man\*.1"
+  RMDir "$INSTDIR\man"
+
+  Delete "$INSTDIR\emacs\*.el"
+  RMDir "$INSTDIR\emacs"
+
+;; Start Menu
+  Delete "$SMPROGRAMS\Coq\Coq.lnk"
+  Delete "$SMPROGRAMS\Coq\CoqIde.lnk"
+  Delete "$SMPROGRAMS\Coq\Uninstall.lnk"
+  Delete "$SMPROGRAMS\Coq\The Coq HomePage.url"
+  Delete "$SMPROGRAMS\Coq\The Coq Standard Library.url"
+  Delete "$INSTDIR\Uninstall.exe"
+  
+  DeleteRegKey /ifempty HKCU "Software\${MY_PRODUCT}"
+
+  DeleteRegKey HKEY_LOCAL_MACHINE "SOFTWARE\Coq"
+  DeleteRegKey HKEY_LOCAL_MACHINE "SOFTWARE\Microsoft\Windows\CurrentVersion\Uninstall\Coq"
+  RMDir "$INSTDIR"
+  RMDir "$SMPROGRAMS\Coq"
+
+  ${unregisterExtension} ".v" "Coq Script File"
+
+SectionEnd
diff --git a/dev/ocamldebug-coq.template b/dev/ocamldebug-coq.run
index 74320588..d4ab22ce 100644
--- a/dev/ocamldebug-coq.template
+++ b/dev/ocamldebug-coq.run
@@ -1,21 +1,24 @@
 #!/bin/sh
 
-# wrap around ocamldebug for Coq
+# Wrapper around ocamldebug for Coq
 
-export COQTOP=COQTOPDIRECTORY
-export COQLIB=COQLIBDIRECTORY
-export COQTH=$COQLIB/theories
-CAMLBIN=CAMLBINDIRECTORY
-CAMLP4LIB=CAMLP4LIBDIRECTORY
-OCAMLDEBUG=$CAMLBIN/ocamldebug
+# This file is to be launched via the generated script ocamldebug-coq,
+# which will set the env variables $OCAMLDEBUG, $CAMLP4LIB, $COQTOP
+# Anyway, just in case someone tries to use this script directly,
+# here are some reasonable default values
+
+[ -z "$OCAMLDEBUG" ] && OCAMLDEBUG=ocamldebug
+[ -z "$CAMLP4LIB" ] && CAMLP4LIB=+camlp5
+[ -z "$COQTOP" -a -d "$PWD/kernel" ] && COQTOP=$PWD
+[ -z "$COQTOP" -a -d "$PWD/../kernel" ] && COQTOP=`dirname $PWD`
 
 exec $OCAMLDEBUG \
 	-I $CAMLP4LIB \
 	-I $COQTOP \
-	-I $COQTOP/config \
-	-I $COQTOP/lib -I $COQTOP/kernel \
+	-I $COQTOP/config -I $COQTOP/printing -I $COQTOP/grammar \
+	-I $COQTOP/lib -I $COQTOP/intf -I $COQTOP/kernel \
 	-I $COQTOP/library -I $COQTOP/pretyping -I $COQTOP/parsing \
-        -I $COQTOP/interp -I $COQTOP/proofs -I $COQTOP/tactics \
+        -I $COQTOP/interp -I $COQTOP/proofs -I $COQTOP/tactics -I $COQTOP/stm \
 	-I $COQTOP/toplevel -I $COQTOP/dev -I $COQTOP/config \
         -I $COQTOP/plugins/cc         -I $COQTOP/plugins/dp \
         -I $COQTOP/plugins/extraction -I $COQTOP/plugins/field \
@@ -28,4 +31,4 @@ exec $OCAMLDEBUG \
         -I $COQTOP/plugins/subtac     -I $COQTOP/plugins/syntax \
         -I $COQTOP/plugins/xml \
         -I $COQTOP/ide \
-	$*
+	"$@"
diff --git a/dev/printers.mllib b/dev/printers.mllib
index 40a5a822..2f78c2e9 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -1,105 +1,166 @@
 Coq_config
 
+Terminal
+Hook
+Canary
+Hashset
+Hashcons
+CSet
+CMap
+Int
+HMap
+Option
+Store
+Exninfo
+Backtrace
+IStream
 Pp_control
-Pp
+Loc
 Compat
 Flags
+Control
+Loc
+Serialize
+Stateid
+Feedback
+Pp
 Segmenttree
 Unicodetable
-Util
+Unicode
 Errors
+CObj
+CList
+CString
+CArray
+CStack
+Util
 Bigint
-Hashcons
 Dyn
+CUnix
 System
 Envars
-Store
-Gmap
-Fset
-Fmap
-Gmapl
+Aux_file
 Profile
 Explore
 Predicate
 Rtree
 Heap
-Option
-Dnet
-Hashtbl_alt
+Genarg
+Stateid
+Ephemeron
+Future
+RemoteCounter
+Monad
 
 Names
 Univ
 Esubst
+Uint31
+Sorts
+Evar
+Constr
+Context
+Vars
 Term
 Mod_subst
-Sign
 Cbytecodes
 Copcodes
 Cemitcodes
-Declarations
+Nativevalues
+Primitives
+Nativeinstr
+Future
+Opaqueproof
+Declareops
 Retroknowledge
+Conv_oracle
 Pre_env
+Nativelambda
+Nativecode
+Nativelib
 Cbytegen
 Environ
-Conv_oracle
 Closure
 Reduction
+Nativeconv
 Type_errors
-Entries
 Modops
 Inductive
 Typeops
+Fast_typeops
 Indtypes
 Cooking
 Term_typing
 Subtyping
 Mod_typing
+Nativelibrary
 Safe_typing
+Unionfind
 
 Summary
 Nameops
 Libnames
+Globnames
 Global
 Nametab
 Libobject
 Lib
+Loadpath
 Goptions
 Decls
 Heads
 Assumptions
+Keys
+Locusops
+Miscops
+Universes
 Termops
 Namegen
 Evd
-Glob_term
+Glob_ops
+Redops
 Reductionops
 Inductiveops
+Arguments_renaming
+Nativenorm
 Retyping
 Cbv
 Pretype_errors
 Evarutil
-Term_dnet
+Evarsolve
 Recordops
 Evarconv
-Arguments_renaming
 Typing
-Pattern
-Matching
+Patternops
+Constr_matching
+Find_subterm
 Tacred
 Classops
 Typeclasses_errors
 Typeclasses
 Detyping
 Indrec
+Program
 Coercion
-Unification
 Cases
 Pretyping
+Unification
 Declaremods
+Library
+States
 
+Genprint
 Tok
 Lexer
 Ppextend
-Genarg
+Pputils
+Ppstyle
+Ppannotation
+Stdarg
+Constrarg
+Constrexpr_ops
+Genintern
+Notation_ops
 Topconstr
 Notation
 Dumpglob
@@ -111,13 +172,16 @@ Smartlocate
 Constrintern
 Modintern
 Constrextern
-Tacexpr
 Proof_type
 Goal
+Miscprint
 Logic
 Refiner
 Clenv
 Evar_refiner
+Proof_errors
+Logic_monad
+Proofview_monad
 Proofview
 Proof
 Proof_global
@@ -125,16 +189,24 @@ Pfedit
 Tactic_debug
 Decl_mode
 Ppconstr
-Extend
-Extrawit
 Pcoq
 Printer
 Pptactic
 Ppdecl_proof
-Tactic_printer
-Egrammar
+Egramml
+Egramcoq
+Tacsubst
+Tacenv
+Trie
+Dn
+Btermdn
+Hints
 Himsg
 Cerrors
-Vernacexpr
+Locality
 Vernacinterp
+Dischargedhypsmap
+Discharge
+Declare
+Ind_tables
 Top_printers
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 0c244603..dea70360 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -8,70 +8,93 @@
 
 (* Printers for the ocaml toplevel. *)
 
-open System
 open Util
 open Pp
 open Names
 open Libnames
+open Globnames
 open Nameops
-open Sign
 open Univ
 open Environ
 open Printer
-open Tactic_printer
 open Term
-open Termops
-open Cerrors
 open Evd
 open Goptions
 open Genarg
-open Mod_subst
 open Clenv
+open Universes
 
-let _ = Constrextern.print_evar_arguments := true
-let _ = Constrextern.print_universes := true
+let _ = Detyping.print_evar_arguments := true
+let _ = Detyping.print_universes := true
 let _ = set_bool_option_value ["Printing";"Matching"] false
 let _ = Detyping.set_detype_anonymous (fun _ _ -> raise Not_found)
 
 (* std_ppcmds *)
 let pppp x = pp x
 
+(** Future printer *)
+
+let ppfuture kx = pp (Future.print (fun _ -> str "_") kx)
+
 (* name printers *)
 let ppid id = pp (pr_id id)
 let pplab l = pp (pr_lab l)
-let ppmbid mbid = pp (str (debug_string_of_mbid mbid))
+let ppmbid mbid = pp (str (MBId.debug_to_string mbid))
 let ppdir dir = pp (pr_dirpath dir)
 let ppmp mp = pp(str (string_of_mp mp))
 let ppcon con = pp(debug_pr_con con)
+let ppproj con = pp(debug_pr_con (Projection.constant con))
 let ppkn kn = pp(pr_kn kn)
 let ppmind kn = pp(debug_pr_mind kn)
+let ppind (kn,i) = pp(debug_pr_mind kn ++ str"," ++int i)
 let ppsp sp = pp(pr_path sp)
 let ppqualid qid = pp(pr_qualid qid)
 let ppclindex cl = pp(Classops.pr_cl_index cl)
+let ppscheme k = pp (Ind_tables.pr_scheme_kind k)
+
+let pprecarg = function
+  | Declarations.Norec -> str "Norec"
+  | Declarations.Mrec (mind,i) ->
+     str "Mrec[" ++ MutInd.print mind ++ pr_comma () ++ int i ++ str "]"
+  | Declarations.Imbr (mind,i) ->
+     str "Imbr[" ++ MutInd.print mind ++ pr_comma () ++ int i ++ str "]"
+let ppwf_paths x = pp (Rtree.pp_tree pprecarg x)
+
+let pprecarg = function
+  | Declarations.Norec -> str "Norec"
+  | Declarations.Mrec (mind,i) ->
+     str "Mrec[" ++ MutInd.print mind ++ pr_comma () ++ int i ++ str "]"
+  | Declarations.Imbr (mind,i) ->
+     str "Imbr[" ++ MutInd.print mind ++ pr_comma () ++ int i ++ str "]"
+let ppwf_paths x = pp (Rtree.pp_tree pprecarg x)
 
 (* term printers *)
 let rawdebug = ref false
+let ppevar evk = pp (str (Evd.string_of_existential evk))
 let ppconstr x = pp (Termops.print_constr x)
+let ppconstr_expr x = pp (Ppconstr.pr_constr_expr x)
 let ppconstrdb x = pp(Flags.with_option rawdebug Termops.print_constr x)
 let ppterm = ppconstr
-let ppsconstr x = ppconstr (Declarations.force x)
+let ppsconstr x = ppconstr (Mod_subst.force_constr x)
 let ppconstr_univ x = Constrextern.with_universes ppconstr x
 let ppglob_constr = (fun x -> pp(pr_lglob_constr x))
 let pppattern = (fun x -> pp(pr_constr_pattern x))
 let pptype = (fun x -> try pp(pr_ltype x) with e -> pp (str (Printexc.to_string e)))
-
 let ppfconstr c = ppconstr (Closure.term_of_fconstr c)
 
 let ppbigint n = pp (str (Bigint.to_string n));;
 
 let prset pr l = str "[" ++ hov 0 (prlist_with_sep spc pr l) ++ str "]"
-let ppintset l = pp (prset int (Intset.elements l))
-let ppidset l = pp (prset pr_id (Idset.elements l))
+let ppintset l = pp (prset int (Int.Set.elements l))
+let ppidset l = pp (prset pr_id (Id.Set.elements l))
 
 let prset' pr l = str "[" ++ hov 0 (prlist_with_sep pr_comma pr l) ++ str "]"
-let ppidmap pr l =
+
+let pridmap pr l =
   let pr (id,b) = pr_id id ++ str "=>" ++ pr id b in
-  pp (prset' pr (Idmap.fold (fun a b l -> (a,b)::l) l []))
+  prset' pr (Id.Map.fold (fun a b l -> (a,b)::l) l [])
+
+let ppidmap pr l = pp (pridmap pr l)
 
 let ppevarsubst = ppidmap (fun id0 -> prset (fun (c,copt,id) ->
   hov 0
@@ -81,6 +104,33 @@ let ppevarsubst = ppidmap (fun id0 -> prset (fun (c,copt,id) ->
    (if id = id0 then mt ()
     else spc () ++ str "<canonical: " ++ pr_id id ++ str ">"))))
 
+let prididmap = pridmap (fun _ -> pr_id)
+let ppididmap = ppidmap (fun _ -> pr_id)
+
+let prconstrunderbindersidmap = pridmap (fun _ (l,c) ->
+  hov 1 (str"[" ++  prlist_with_sep spc Id.print l ++ str"]")
+  ++ str "," ++ spc () ++ Termops.print_constr c)
+
+let ppconstrunderbindersidmap l = pp (prconstrunderbindersidmap l)
+
+let ppunbound_ltac_var_map l = ppidmap (fun _ arg ->
+  str"<genarg:" ++ pr_argument_type(genarg_tag arg) ++ str">")
+
+open Glob_term
+
+let rec pr_closure {idents=idents;typed=typed;untyped=untyped} =
+  hov 1 (str"{idents=" ++ prididmap idents ++ str";" ++ spc() ++
+         str"typed=" ++ prconstrunderbindersidmap typed ++ str";" ++ spc() ++
+         str"untyped=" ++ pr_closed_glob_constr_idmap untyped ++ str"}")
+and pr_closed_glob_constr_idmap x =
+  pridmap (fun _ -> pr_closed_glob_constr) x
+and pr_closed_glob_constr {closure=closure;term=term} =
+  pr_closure closure ++ pr_lglob_constr term
+
+let ppclosure x = pp (pr_closure x)
+let ppclosedglobconstr x = pp (pr_closed_glob_constr x)
+let ppclosedglobconstridmap x = pp (pr_closed_glob_constr_idmap x)
+
 let pP s = pp (hov 0 s)
 
 let safe_pr_global = function
@@ -109,18 +159,33 @@ let prdelta s = pp (Mod_subst.debug_pr_delta s)
 let pp_idpred s = pp (pr_idpred s)
 let pp_cpred s = pp (pr_cpred s)
 let pp_transparent_state s = pp (pr_transparent_state s)
+let pp_stack_t n = pp (Reductionops.Stack.pr Termops.print_constr n)
+let pp_cst_stack_t n = pp (Reductionops.Cst_stack.pr n)
+let pp_state_t n = pp (Reductionops.pr_state n)
 
 (* proof printers *)
+let pr_evar ev = Pp.int (Evar.repr ev)
 let ppmetas metas = pp(pr_metaset metas)
-let ppevm evd = pp(pr_evar_map (Some 2) evd)
-let ppevmall evd = pp(pr_evar_map None evd)
+let ppevm evd = pp(pr_evar_map ~with_univs:!Flags.univ_print (Some 2) evd)
+let ppevmall evd = pp(pr_evar_map ~with_univs:!Flags.univ_print None evd)
 let pr_existentialset evars =
-  prlist_with_sep spc pr_meta (ExistentialSet.elements evars)
+  prlist_with_sep spc pr_evar (Evar.Set.elements evars)
 let ppexistentialset evars =
   pp (pr_existentialset evars)
+let ppexistentialfilter filter = match Evd.Filter.repr filter with
+| None -> pp (Pp.str "ø")
+| Some f -> pp (prlist_with_sep spc bool f)
 let ppclenv clenv = pp(pr_clenv clenv)
 let ppgoalgoal gl = pp(Goal.pr_goal gl)
 let ppgoal g = pp(Printer.pr_goal g)
+let ppgoalsigma g = pp(Printer.pr_goal g ++ pr_evar_map None (Refiner.project g))
+let pphintdb db = pp(Hints.pr_hint_db db)
+let ppproofview p =
+  let gls,sigma = Proofview.proofview p in
+  pp(pr_enum Goal.pr_goal gls ++ fnl () ++ pr_evar_map (Some 1) sigma)
+
+let ppopenconstr (x : Evd.open_constr) =
+  let (evd,c) = x in pp (pr_evar_map (Some 2) evd ++ pr_constr c)
 (* spiwack: deactivated until a replacement is found
 let pppftreestate p = pp(print_pftreestate p)
 *)
@@ -131,7 +196,7 @@ let pppftreestate p = pp(print_pftreestate p)
 
 (* let pr_glls glls = *)
 (*   hov 0 (pr_evar_defs (sig_sig glls) ++ fnl () ++ *)
-(*          prlist_with_sep pr_fnl db_pr_goal (sig_it glls)) *)
+(*          prlist_with_sep fnl db_pr_goal (sig_it glls)) *)
 
 (* let ppsigmagoal g = pp(pr_goal (sig_it g)) *)
 (* let prgls gls = pp(pr_gls gls) *)
@@ -139,19 +204,34 @@ let pppftreestate p = pp(print_pftreestate p)
 (* let pproof p = pp(print_proof Evd.empty empty_named_context p) *)
 
 let ppuni u = pp(pr_uni u)
-
-let ppuniverses u = pp (str"[" ++ pr_universes u ++ str"]")
-
-let ppconstraints c = pp (pr_constraints c)
+let ppuni_level u = pp (Level.pr u)
+let ppuniverse u = pp (str"[" ++ Universe.pr u ++ str"]")
+
+let prlev = Universes.pr_with_global_universes
+let ppuniverse_set l = pp (LSet.pr prlev l)
+let ppuniverse_instance l = pp (Instance.pr prlev l)
+let ppuniverse_context l = pp (pr_universe_context prlev l)
+let ppuniverse_context_set l = pp (pr_universe_context_set prlev l)
+let ppuniverse_subst l = pp (Univ.pr_universe_subst l)
+let ppuniverse_opt_subst l = pp (Universes.pr_universe_opt_subst l)
+let ppuniverse_level_subst l = pp (Univ.pr_universe_level_subst l)
+let ppevar_universe_context l = pp (Evd.pr_evar_universe_context l)
+let ppconstraints_map c = pp (Universes.pr_constraints_map c)
+let ppconstraints c = pp (pr_constraints Level.pr c)
+let ppuniverseconstraints c = pp (Universes.Constraints.pr c)
+let ppuniverse_context_future c = 
+  let ctx = Future.force c in
+    ppuniverse_context ctx
+let ppuniverses u = pp (Univ.pr_universes Level.pr u)
+let ppnamedcontextval e =
+  pp (pr_named_context (Global.env ()) Evd.empty (named_context_of_val e))
 
 let ppenv e = pp
-  (str "[" ++ pr_named_context_of e ++ str "]" ++ spc() ++
-   str "[" ++ pr_rel_context e (rel_context e) ++ str "]")
+  (str "[" ++ pr_named_context_of e Evd.empty ++ str "]" ++ spc() ++
+   str "[" ++ pr_rel_context e Evd.empty (rel_context e) ++ str "]")
 
 let pptac = (fun x -> pp(Pptactic.pr_glob_tactic (Global.env()) x))
 
-let ppinsts c = pp (pr_instance_gmap c)
-
 let ppobj obj = Format.print_string (Libobject.object_tag obj)
 
 let cnt = ref 0
@@ -161,12 +241,13 @@ let cast_kind_display k =
   | VMcast -> "VMcast"
   | DEFAULTcast -> "DEFAULTcast"
   | REVERTcast -> "REVERTcast"
+  | NATIVEcast -> "NATIVEcast"
 
 let constr_display csr =
   let rec term_display c = match kind_of_term c with
   | Rel n -> "Rel("^(string_of_int n)^")"
   | Meta n -> "Meta("^(string_of_int n)^")"
-  | Var id -> "Var("^(string_of_id id)^")"
+  | Var id -> "Var("^(Id.to_string id)^")"
   | Sort s -> "Sort("^(sort_display s)^")"
   | Cast (c,k, t) ->
       "Cast("^(term_display c)^","^(cast_kind_display k)^","^(term_display t)^")"
@@ -178,13 +259,14 @@ let constr_display csr =
       "LetIn("^(name_display na)^","^(term_display b)^","
       ^(term_display t)^","^(term_display c)^")"
   | App (c,l) -> "App("^(term_display c)^","^(array_display l)^")\n"
-  | Evar (e,l) -> "Evar("^(string_of_int e)^","^(array_display l)^")"
-  | Const c -> "Const("^(string_of_con c)^")"
-  | Ind (sp,i) ->
-      "MutInd("^(string_of_mind sp)^","^(string_of_int i)^")"
-  | Construct ((sp,i),j) ->
+  | Evar (e,l) -> "Evar("^(string_of_existential e)^","^(array_display l)^")"
+  | Const (c,u) -> "Const("^(string_of_con c)^","^(universes_display u)^")"
+  | Ind ((sp,i),u) ->
+      "MutInd("^(string_of_mind sp)^","^(string_of_int i)^","^(universes_display u)^")"
+  | Construct (((sp,i),j),u) ->
       "MutConstruct(("^(string_of_mind sp)^","^(string_of_int i)^"),"
-      ^(string_of_int j)^")"
+      ^","^(universes_display u)^(string_of_int j)^")"
+  | Proj (p, c) -> "Proj("^(string_of_con (Projection.constant p))^","^term_display c ^")"
   | Case (ci,p,c,bl) ->
       "MutCase(<abs>,"^(term_display p)^","^(term_display c)^","
       ^(array_display bl)^")"
@@ -208,19 +290,28 @@ let constr_display csr =
        (fun x i -> (term_display x)^(if not(i="") then (";"^i) else ""))
        v "")^"|]"
 
+  and univ_display u =
+    incr cnt; pp (str "with " ++ int !cnt ++ str" " ++ pr_uni u ++ fnl ())
+
+  and level_display u =
+    incr cnt; pp (str "with " ++ int !cnt ++ str" " ++ Level.pr u ++ fnl ())
+
   and sort_display = function
     | Prop(Pos) -> "Prop(Pos)"
     | Prop(Null) -> "Prop(Null)"
-    | Type u ->
-	incr cnt; pp (str "with " ++ int !cnt ++ pr_uni u ++ fnl ());
+    | Type u -> univ_display u;
 	"Type("^(string_of_int !cnt)^")"
 
+  and universes_display l = 
+    Array.fold_right (fun x i -> level_display x; (string_of_int !cnt)^(if not(i="")
+        then (" "^i) else "")) (Instance.to_array l) ""
+
   and name_display = function
-    | Name id -> "Name("^(string_of_id id)^")"
+    | Name id -> "Name("^(Id.to_string id)^")"
     | Anonymous -> "Anonymous"
 
   in
-    msg (str (term_display csr) ++fnl ())
+  Pp.pp (str (term_display csr) ++fnl ()); Pp.pp_flush ()
 
 open Format;;
 
@@ -228,14 +319,14 @@ let print_pure_constr csr =
   let rec term_display c = match kind_of_term c with
   | Rel n -> print_string "#"; print_int n
   | Meta n -> print_string "Meta("; print_int n; print_string ")"
-  | Var id -> print_string (string_of_id id)
+  | Var id -> print_string (Id.to_string id)
   | Sort s -> sort_display s
   | Cast (c,_, t) -> open_hovbox 1;
       print_string "("; (term_display c); print_cut();
       print_string "::"; (term_display t); print_string ")"; close_box()
   | Prod (Name(id),t,c) ->
       open_hovbox 1;
-      print_string"("; print_string (string_of_id id);
+      print_string"("; print_string (Id.to_string id);
       print_string ":"; box_display t;
       print_string ")"; print_cut();
       box_display c; close_box()
@@ -256,22 +347,31 @@ let print_pure_constr csr =
       box_display c;
       Array.iter (fun x -> print_space (); box_display x) l;
       print_string ")"
-  | Evar (e,l) -> print_string "Evar#"; print_int e; print_string "{";
+  | Evar (e,l) -> print_string "Evar#"; print_int (Evar.repr e); print_string "{";
       Array.iter (fun x -> print_space (); box_display x) l;
       print_string"}"
-  | Const c -> print_string "Cons(";
+  | Const (c,u) -> print_string "Cons(";
       sp_con_display c;
+      print_string ","; universes_display u;
       print_string ")"
-  | Ind (sp,i) ->
+  | Proj (p,c') -> print_string "Proj(";
+      sp_con_display (Projection.constant p);
+      print_string ",";
+      box_display c';
+      print_string ")"
+  | Ind ((sp,i),u) ->
       print_string "Ind(";
       sp_display sp;
       print_string ","; print_int i;
+      print_string ","; universes_display u;
       print_string ")"
-  | Construct ((sp,i),j) ->
+  | Construct (((sp,i),j),u) ->
       print_string "Constr(";
       sp_display sp;
       print_string ",";
-      print_int i; print_string ","; print_int j; print_string ")"
+      print_int i; print_string ","; print_int j; 
+      print_string ","; universes_display u;
+      print_string ")"
   | Case (ci,p,c,bl) ->
       open_vbox 0;
       print_string "<"; box_display p; print_string ">";
@@ -287,7 +387,7 @@ let print_pure_constr csr =
       print_string "Fix("; print_int i; print_string ")";
       print_cut();
       open_vbox 0;
-      let rec print_fix () =
+      let print_fix () =
         for k = 0 to (Array.length tl) - 1 do
 	  open_vbox 0;
 	  name_display lna.(k); print_string "/";
@@ -301,7 +401,7 @@ let print_pure_constr csr =
       print_string "CoFix("; print_int i; print_string ")";
       print_cut();
       open_vbox 0;
-      let rec print_fix () =
+      let print_fix () =
         for k = 0 to (Array.length tl) - 1 do
           open_vbox 1;
 	  name_display lna.(k);  print_cut(); print_string ":";
@@ -313,6 +413,9 @@ let print_pure_constr csr =
 
   and box_display c = open_hovbox 1; term_display c; close_box()
 
+  and universes_display u =
+    Array.iter (fun u -> print_space (); pp (Level.pr u)) (Instance.to_array u)
+
   and sort_display = function
     | Prop(Pos) -> print_string "Set"
     | Prop(Null) -> print_string "Prop"
@@ -320,13 +423,13 @@ let print_pure_constr csr =
 	print_string "Type("; pp (pr_uni u); print_string ")"; close_box()
 
   and name_display = function
-    | Name id -> print_string (string_of_id id)
+    | Name id -> print_string (Id.to_string id)
     | Anonymous -> print_string "_"
 (* Remove the top names for library and Scratch to avoid long names *)
   and sp_display sp =
 (*    let dir,l = decode_kn sp in
     let ls =
-      match List.rev (List.map string_of_id (repr_dirpath dir)) with
+      match List.rev_map Id.to_string (DirPath.repr dir) with
           ("Top"::l)-> l
 	| ("Coq"::_::l) -> l
 	| l             -> l
@@ -335,7 +438,7 @@ let print_pure_constr csr =
   and sp_con_display sp =
 (*    let dir,l = decode_kn sp in
     let ls =
-      match List.rev (List.map string_of_id (repr_dirpath dir)) with
+      match List.rev_map Id.to_string (DirPath.repr dir) with
           ("Top"::l)-> l
 	| ("Coq"::_::l) -> l
 	| l             -> l
@@ -351,43 +454,29 @@ let print_pure_constr csr =
 
 let ppfconstr c = ppconstr (Closure.term_of_fconstr c)
 
-let pploc x = let (l,r) = unloc x in
+let pploc x = let (l,r) = Loc.unloc x in
   print_string"(";print_int l;print_string",";print_int r;print_string")"
 
-(* extendable tactic arguments *)
-let rec pr_argument_type = function
-  (* Basic types *)
-  | BoolArgType -> str"bool"
-  | IntArgType -> str"int"
-  | IntOrVarArgType -> str"int-or-var"
-  | StringArgType -> str"string"
-  | PreIdentArgType -> str"pre-ident"
-  | IntroPatternArgType -> str"intro-pattern"
-  | IdentArgType true -> str"ident"
-  | IdentArgType false -> str"pattern_ident"
-  | VarArgType -> str"var"
-  | RefArgType -> str"ref"
-  (* Specific types *)
-  | SortArgType -> str"sort"
-  | ConstrArgType -> str"constr"
-  | ConstrMayEvalArgType -> str"constr-may-eval"
-  | QuantHypArgType -> str"qhyp"
-  | OpenConstrArgType _ -> str"open-constr"
-  | ConstrWithBindingsArgType -> str"constr-with-bindings"
-  | BindingsArgType -> str"bindings"
-  | RedExprArgType -> str"redexp"
-  | List0ArgType t -> pr_argument_type t ++ str" list0"
-  | List1ArgType t -> pr_argument_type t ++ str" list1"
-  | OptArgType t -> pr_argument_type t ++ str" opt"
-  | PairArgType (t1,t2) ->
-      str"("++ pr_argument_type t1 ++ str"*" ++ pr_argument_type t2 ++str")"
-  | ExtraArgType s -> str"\"" ++ str s ++ str "\""
-
 let pp_argument_type t = pp (pr_argument_type t)
 
 let pp_generic_argument arg =
   pp(str"<genarg:"++pr_argument_type(genarg_tag arg)++str">")
 
+let prgenarginfo arg =
+  let tpe = pr_argument_type (genarg_tag arg) in
+  let pr_gtac _ x = Pptactic.pr_glob_tactic (Global.env()) x in
+  try
+    let data = Pptactic.pr_top_generic pr_constr pr_lconstr pr_gtac pr_constr_pattern arg in
+    str "<genarg:" ++ tpe ++ str " := [ " ++ data ++ str " ] >"
+  with _any ->
+    str "<genarg:" ++ tpe ++ str ">"
+
+let ppgenarginfo arg = pp (prgenarginfo arg)
+
+let ppist ist =
+  let pr id arg = prgenarginfo arg in
+  pp (pridmap pr ist.Geninterp.lfun)
+
 (**********************************************************************)
 (* Vernac-level debugging commands                                    *)
 
@@ -395,7 +484,7 @@ let in_current_context f c =
   let (evmap,sign) =
     try Pfedit.get_current_goal_context ()
     with e when Logic.catchable_exception e -> (Evd.empty, Global.env()) in
-  f (Constrintern.interp_constr evmap sign c)
+  f (fst (Constrintern.interp_constr sign evmap c))(*FIXME*)
 
 (* We expand the result of preprocessing to be independent of camlp4
 
@@ -409,87 +498,87 @@ END
 
 open Pcoq
 open Genarg
-open Egrammar
+open Constrarg
+open Egramml
 
 let _ =
   try
-    Vernacinterp.vinterp_add "PrintConstr"
+    Vernacinterp.vinterp_add ("PrintConstr", 0)
       (function
          [c] when genarg_tag c = ConstrArgType && true ->
-           let c = out_gen rawwit_constr c in
+           let c = out_gen (rawwit wit_constr) c in
            (fun () -> in_current_context constr_display c)
        | _ -> failwith "Vernac extension: cannot occur")
   with
     e -> Pp.pp (Errors.print e)
 let _ =
-  extend_vernac_command_grammar "PrintConstr" None
-    [[GramTerminal "PrintConstr";
+  extend_vernac_command_grammar ("PrintConstr", 0) None
+    [GramTerminal "PrintConstr";
       GramNonTerminal
-        (dummy_loc,ConstrArgType,Aentry ("constr","constr"),
-	 Some (Names.id_of_string "c"))]]
+        (Loc.ghost,ConstrArgType,Aentry ("constr","constr"),
+	 Some (Names.Id.of_string "c"))]
 
 let _ =
   try
-    Vernacinterp.vinterp_add "PrintPureConstr"
+    Vernacinterp.vinterp_add ("PrintPureConstr", 0)
       (function
          [c] when genarg_tag c = ConstrArgType && true ->
-           let c = out_gen rawwit_constr c in
+           let c = out_gen (rawwit wit_constr) c in
            (fun () -> in_current_context print_pure_constr c)
        | _ -> failwith "Vernac extension: cannot occur")
   with
     e -> Pp.pp (Errors.print e)
 let _ =
-  extend_vernac_command_grammar "PrintPureConstr" None
-    [[GramTerminal "PrintPureConstr";
+  extend_vernac_command_grammar ("PrintPureConstr", 0) None
+    [GramTerminal "PrintPureConstr";
       GramNonTerminal
-        (dummy_loc,ConstrArgType,Aentry ("constr","constr"),
-	 Some (Names.id_of_string "c"))]]
+        (Loc.ghost,ConstrArgType,Aentry ("constr","constr"),
+	 Some (Names.Id.of_string "c"))]
 
 (* Setting printer of unbound global reference *)
 open Names
-open Nameops
 open Libnames
 
 let encode_path loc prefix mpdir suffix id =
   let dir = match mpdir with
     | None -> []
     | Some (mp,dir) ->
-	(repr_dirpath (dirpath_of_string (string_of_mp mp))@
-	repr_dirpath dir) in
+	(DirPath.repr (dirpath_of_string (string_of_mp mp))@
+	DirPath.repr dir) in
   Qualid (loc, make_qualid
-    (make_dirpath (List.rev (id_of_string prefix::dir@suffix))) id)
+    (DirPath.make (List.rev (Id.of_string prefix::dir@suffix))) id)
 
 let raw_string_of_ref loc _ = function
   | ConstRef cst ->
       let (mp,dir,id) = repr_con cst in
-      encode_path loc "CST" (Some (mp,dir)) [] (id_of_label id)
+      encode_path loc "CST" (Some (mp,dir)) [] (Label.to_id id)
   | IndRef (kn,i) ->
       let (mp,dir,id) = repr_mind kn in
-      encode_path loc "IND" (Some (mp,dir)) [id_of_label id]
-	(id_of_string ("_"^string_of_int i))
+      encode_path loc "IND" (Some (mp,dir)) [Label.to_id id]
+	(Id.of_string ("_"^string_of_int i))
   | ConstructRef ((kn,i),j) ->
       let (mp,dir,id) = repr_mind kn in
       encode_path loc "CSTR" (Some (mp,dir))
-	[id_of_label id;id_of_string ("_"^string_of_int i)]
-	(id_of_string ("_"^string_of_int j))
+	[Label.to_id id;Id.of_string ("_"^string_of_int i)]
+	(Id.of_string ("_"^string_of_int j))
   | VarRef id ->
       encode_path loc "SECVAR" None [] id
 
 let short_string_of_ref loc _ = function
   | VarRef id -> Ident (loc,id)
-  | ConstRef cst -> Ident (loc,id_of_label (pi3 (repr_con cst)))
-  | IndRef (kn,0) -> Ident (loc,id_of_label (pi3 (repr_mind kn)))
+  | ConstRef cst -> Ident (loc,Label.to_id (pi3 (repr_con cst)))
+  | IndRef (kn,0) -> Ident (loc,Label.to_id (pi3 (repr_mind kn)))
   | IndRef (kn,i) ->
-      encode_path loc "IND" None [id_of_label (pi3 (repr_mind kn))]
-        (id_of_string ("_"^string_of_int i))
+      encode_path loc "IND" None [Label.to_id (pi3 (repr_mind kn))]
+        (Id.of_string ("_"^string_of_int i))
   | ConstructRef ((kn,i),j) ->
       encode_path loc "CSTR" None
-        [id_of_label (pi3 (repr_mind kn));id_of_string ("_"^string_of_int i)]
-        (id_of_string ("_"^string_of_int j))
+        [Label.to_id (pi3 (repr_mind kn));Id.of_string ("_"^string_of_int i)]
+        (Id.of_string ("_"^string_of_int j))
 
 (* Anticipate that printers can be used from ocamldebug and that 
    pretty-printer should not make calls to the global env since ocamldebug
    runs in a different process and does not have the proper env at hand *)
-let _ = Constrextern.in_debugger := true
+let _ = Flags.in_debugger := true
 let _ = Constrextern.set_extern_reference
   (if !rawdebug then raw_string_of_ref else short_string_of_ref)
diff --git a/dev/vm_printers.ml b/dev/vm_printers.ml
index 59545d8a..4578a3b3 100644
--- a/dev/vm_printers.ml
+++ b/dev/vm_printers.ml
@@ -13,7 +13,7 @@ let ppripos (ri,pos) =
 	("annot : MutInd("^(string_of_mind sp)^","^(string_of_int i)^")\n")
   | Reloc_const _ ->
       print_string "structured constant\n"
-  | Reloc_getglobal kn ->
+  | Reloc_getglobal (kn,_) ->
       print_string ("getglob "^(string_of_con kn)^"\n"));
    print_flush ()
 
@@ -30,11 +30,11 @@ let ppsort = function
 
 let print_idkey idk =
   match idk with
-  | ConstKey sp ->
+  | ConstKey (sp,_) ->
       print_string "Cons(";
       print_string (string_of_con sp);
       print_string ")"
-  | VarKey id -> print_string (string_of_id id)
+  | VarKey id -> print_string (Id.to_string id)
   | RelKey i -> print_string "~";print_int i
 
 let rec ppzipper z =
@@ -61,7 +61,7 @@ and ppatom a =
   match a with
   | Aid idk -> print_idkey idk
   | Aiddef(idk,_) -> print_string "&";print_idkey idk
-  | Aind(sp,i) ->  print_string "Ind(";
+  | Aind((sp,i),_) ->  print_string "Ind(";
       print_string (string_of_mind sp);
       print_string ","; print_int i;
       print_string ")"