Merge branch 'experimental/upstream' into experimental/master

20 files changed, 1484 insertions, 122 deletions

diff --git a/dev/base_include b/dev/base_include
index 711dcb2a..3a31230f 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -53,6 +53,7 @@
 open Names
 open Term
 open Typeops
+open Term_typing
 open Univ
 open Inductive
 open Indtypes
@@ -89,6 +90,7 @@ open Evarutil
 open Tacred
 open Evd
 open Termops
+open Namegen
 open Indrec
 open Typing
 open Inductiveops
@@ -105,6 +107,8 @@ open Ppextend
 open Reserve
 open Syntax_def
 open Topconstr
+open Prettyp
+open Search
 
 open Clenvtac
 open Evar_refiner
@@ -137,10 +141,15 @@ open Refine
 open Tacinterp
 open Tacticals
 open Tactics
+open Eqschemes
 
 open Cerrors
 open Class
 open Command
+open Indschemes
+open Ind_tables
+open Auto_ind_decl
+open Lemmas
 open Coqinit
 open Coqtop
 open Discharge
@@ -180,7 +189,7 @@ let constr_of_string s =
 open Declarations;;
 
 let constbody_of_string s =
-  let b = Global.lookup_constant (Nametab.locate_constant (qualid_of_sp (path_of_string s))) in
+  let b = Global.lookup_constant (Nametab.locate_constant (qualid_of_string s)) in
   Option.get b.const_body;;
 
 (* Get the current goal *)
diff --git a/dev/db b/dev/db
index 81878570..22b76605 100644
--- a/dev/db
+++ b/dev/db
@@ -3,14 +3,15 @@ load_printer "printers.cma"
 
 install_printer Top_printers.ppid
 install_printer Top_printers.ppidset
+install_printer Top_printers.ppevarsubst
 install_printer Top_printers.ppintset
 install_printer Top_printers.pplab
-install_printer Top_printers.ppmsid
 install_printer Top_printers.ppmbid
 install_printer Top_printers.ppdir
 install_printer Top_printers.ppmp
 install_printer Top_printers.ppkn
 install_printer Top_printers.ppcon
+install_printer Top_printers.ppmind
 install_printer Top_printers.ppsp
 install_printer Top_printers.ppqualid
 install_printer Top_printers.ppclindex
@@ -31,7 +32,6 @@ install_printer Top_printers.ppgoal
 install_printer Top_printers.ppsigmagoal
 install_printer Top_printers.pproof
 install_printer Top_printers.ppmetas
-install_printer Top_printers.ppevd
 install_printer Top_printers.ppevm
 install_printer Top_printers.ppclenv
 
@@ -39,5 +39,5 @@ install_printer Top_printers.pptac
 install_printer Top_printers.ppobj
 install_printer Top_printers.pploc
 install_printer Top_printers.prsubst
-                                                  
-
+install_printer Top_printers.prdelta
+install_printer Top_printers.ppconstr
diff --git a/dev/doc/build-system.dev.txt b/dev/doc/build-system.dev.txt
index c825f088..d4014303 100644
--- a/dev/doc/build-system.dev.txt
+++ b/dev/doc/build-system.dev.txt
@@ -12,6 +12,7 @@ see build-system.txt .
 happy only. To ensure they are not used for compilation, they contain
 invalid OCaml.
 
+
 multi-stage build
 -----------------
 
@@ -37,6 +38,7 @@ Le Makefile a été séparé en plusieurs fichiers :
 The build needs to be cut in stages because make will not take into
 account one include when making another include.
 
+
 Parallélisation
 ---------------
 
@@ -68,3 +70,62 @@ d'étape pour chaque fichier:
 
 Mais seule la première est gérée explicitement, la seconde est
 implicite.
+
+
+FIND_VCS_CLAUSE
+---------------
+
+The recommended style of using FIND_VCS_CLAUSE is for example
+
+ find . $(FIND_VCS_CLAUSE) '(' -name '*.example' ')' -print
+ find . $(FIND_VCS_CLAUSE) '(' -name '*.example' -or -name '*.foo' ')' -print
+
+1)
+The parentheses even in the one-criteria case is so that if one adds
+other conditions, e.g. change the first example to the second
+
+ find . $(FIND_VCS_CLAUSE) '(' -name '*.example' -and -not -name '*.bak.example' ')' -print
+
+one is not tempted to write
+
+ find . $(FIND_VCS_CLAUSE) -name '*.example' -and -not -name '*.bak.example' -print
+
+because this will not necessarily work as expected; $(FIND_VCS_CLAUSE)
+ends with an -or, and how it combines with what comes later depends on
+operator precedence and all that. Much safer to override it with
+parentheses.
+
+In short, it protects against the -or one doesn't see.
+
+2)
+As to the -print at the end, yes it is necessary. Here's why.
+
+You are used to write:
+ find . -name '*.example'
+and it works fine. But the following will not:
+ find . $(FIND_VCS_CLAUSE) -name '*.example'
+it will also list things directly matched by FIND_VCS_CLAUSE
+(directories we want to prune, in which we don't want to find
+anything). C'est subtil... Il y a effectivement un -print implicite à
+la fin, qui fait que la commande habituelle sans print fonctionne
+bien, mais dès que l'on introduit d'autres commandes dans le lot (le
+-prune de FIND_VCS_CLAUSE), ça se corse à cause d'histoires de
+parenthèses du -print implicite par rapport au parenthésage dans la
+forme recommandée d'utilisation:
+
+Si on explicite le -print et les parenthèses implicites, cela devient:
+
+find . '(' '(' '(' -name .git -or -name debian ')' -prune ')' -or \
+           '(' -name '*.example' ')'
+       ')'
+       -print
+
+Le print agit TOUT ce qui précède, soit sur ce qui matche "'(' -name
+.git -or -name debian ')'" ET sur ce qui matche "'(' -name '*.example' ')'".
+
+alors qu'ajouter le print explicite change cela en
+
+find . '(' '(' -name .git -or -name debian ')' -prune ')' -or \
+       '(' '(' -name '*.example' ')' -print ')'
+
+Le print n'agit plus que sur ce qui matche "'(' -name '*.example' ')'"
diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index cae948a0..91255202 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -1,4 +1,114 @@
 =========================================
+= CHANGES BETWEEN COQ V8.2 AND COQ V8.3 =
+=========================================
+
+** Light cleaning in evarutil.ml **
+
+whd_castappevar is now whd_head_evar
+obsolete whd_ise disappears
+
+** Semantical change of h_induction_destruct **
+
+Warning, the order of the isrec and evar_flag was inconsistent and has
+been permuted. Tactic induction_destruct in tactics.ml is unchanged.
+
+** Internal tactics renamed
+
+There is no more difference between bindings and ebindings. The
+following tactics are therefore renamed
+
+apply_with_ebindings_gen -> apply_with_bindings_gen
+left_with_ebindings -> left_with_bindings
+right_with_ebindings -> right_with_bindings
+split_with_ebindings -> split_with_bindings
+
+and the following tactics are removed
+
+apply_with_ebindings (use instead apply_with_bindings)
+eapply_with_ebindings (use instead eapply_with_bindings)
+
+** Obsolete functions in typing.ml
+
+For mtype_of, msort_of, mcheck, now use type_of, sort_of, check
+
+** Renaming functions renamed
+
+concrete_name -> compute_displayed_name_in
+concrete_let_name -> compute_displayed_let_name_in
+rename_rename_bound_var -> rename_bound_vars_as_displayed
+lookup_name_as_renamed -> lookup_name_as_displayed
+next_global_ident_away true -> next_ident_away_in_goal
+next_global_ident_away false -> next_global_ident_away
+
+** Cleaning in commmand.ml
+
+Functions about starting/ending a lemma are in lemmas.ml
+Functions about inductive schemes are in indschemes.ml
+
+Functions renamed:
+
+declare_one_assumption -> declare_assumption
+declare_assumption -> declare_assumptions
+Command.syntax_definition -> Metasyntax.add_syntactic_definition
+declare_interning_data merged with add_notation_interpretation
+compute_interning_datas -> compute_full_internalization_env
+implicits_env -> internalization_env
+full_implicits_env -> full_internalization_env
+build_mutual -> do_mutual_inductive
+build_recursive -> do_fixpoint
+build_corecursive -> do_cofixpoint
+build_induction_scheme -> build_mutual_induction_scheme
+build_indrec -> build_induction_scheme
+instantiate_type_indrec_scheme -> weaken_sort_scheme
+instantiate_indrec_scheme -> modify_sort_scheme
+make_case_dep, make_case_nodep -> build_case_analysis_scheme
+make_case_gen -> build_case_analysis_scheme_default
+
+Types:
+
+decl_notation -> decl_notation option
+
+** Cleaning in libnames/nametab interfaces
+
+Functions:
+
+dirpath_prefix -> pop_dirpath
+extract_dirpath_prefix pop_dirpath_n
+extend_dirpath -> add_dirpath_suffix
+qualid_of_sp -> qualid_of_path
+pr_sp -> pr_path
+make_short_qualid -> qualid_of_ident
+sp_of_syntactic_definition -> path_of_syntactic_definition 
+sp_of_global -> path_of_global
+id_of_global -> basename_of_global
+absolute_reference -> global_of_path
+locate_syntactic_definition -> locate_syndef
+path_of_syntactic_definition -> path_of_syndef
+push_syntactic_definition -> push_syndef
+
+Types:
+
+section_path -> full_path
+
+** Cleaning in parsing extensions (commit 12108)
+
+Many moves and renamings, one new file (Extrawit, that contains wit_tactic).
+
+** Cleaning in tactical.mli
+
+tclLAST_HYP -> onLastHyp
+tclLAST_DECL -> onLastDecl
+tclLAST_NHYPS -> onNLastHypsId
+tclNTH_DECL -> onNthDecl
+tclNTH_HYP -> onNthHyp
+onLastHyp -> onLastHypId
+onNLastHyps -> onNLastDecls
+onClauses -> onClause
+allClauses -> allHypsAndConcl
+
++ removal of various unused combinators on type "clause"
+
+=========================================
 = CHANGES BETWEEN COQ V8.1 AND COQ V8.2 =
 =========================================
 
@@ -8,7 +118,8 @@ A few differences in Coq ML interfaces between Coq V8.1 and V8.2
 ** Datatypes
 
 List of occurrences moved from "int list" to "Termops.occurrences" (an
-alias to "bool * int list").
+  alias to "bool * int list")
+ETIdent renamed to ETName
 
 ** Functions
 
@@ -325,7 +436,7 @@ Proof_type: subproof field in type proof_tree glued with the ref field
 
 Tacmach: no more echo from functions of module Refiner
 
-Files contrib/*/g_*.ml4 take the place of files contrib/*/*.v.
+Files plugins/*/g_*.ml4 take the place of files plugins/*/*.v.
 Files parsing/{vernac,tac}extend.ml{4,i} implements TACTIC EXTEND andd
   VERNAC COMMAND EXTEND macros
 File syntax/PPTactic.v moved to parsing/pptactic.ml
diff --git a/dev/doc/debugging.txt b/dev/doc/debugging.txt
index e5c83139..50b3b45c 100644
--- a/dev/doc/debugging.txt
+++ b/dev/doc/debugging.txt
@@ -4,8 +4,8 @@ Debugging from Coq toplevel using Caml trace mechanism
   1. Launch bytecode version of Coq (coqtop.byte or coqtop -byte)
   2. Access Ocaml toplevel using vernacular command 'Drop.'
   3. Install load paths and pretty printers for terms, idents, ... using
-     Ocaml command '#use "base_include";;' (use '#use "include";;' for a rawer
-     term pretty printer)
+     Ocaml command '#use "base_include";;' (use '#use "include";;' for 
+     installing the advanced term pretty printers)
   4. Use #trace to tell which function(s) to trace
   5. Go back to Coq toplevel with 'go();;'
   6. Test your Coq command and observe the result of tracing your functions
@@ -15,6 +15,15 @@ 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/naming-conventions.tex b/dev/doc/naming-conventions.tex
new file mode 100644
index 00000000..e7c8975b
--- /dev/null
+++ b/dev/doc/naming-conventions.tex
@@ -0,0 +1,606 @@
+\documentclass[a4paper]{article}
+\usepackage{fullpage}
+\usepackage[latin1]{inputenc}
+\usepackage[T1]{fontenc}
+\usepackage{amsfonts}
+
+\parindent=0pt
+\parskip=10pt
+
+%%%%%%%%%%%%%
+% Macros
+\newcommand\itemrule[3]{
+\subsubsection{#1}
+\begin{quote}
+\begin{tt}
+#3
+\end{tt}
+\end{quote}
+\begin{quote}
+Name: \texttt{#2}
+\end{quote}}
+
+\newcommand\formula[1]{\begin{tt}#1\end{tt}}
+\newcommand\tactic[1]{\begin{tt}#1\end{tt}}
+\newcommand\command[1]{\begin{tt}#1\end{tt}}
+\newcommand\term[1]{\begin{tt}#1\end{tt}}
+\newcommand\library[1]{\texttt{#1}}
+\newcommand\name[1]{\texttt{#1}}
+
+\newcommand\zero{\texttt{zero}}
+\newcommand\op{\texttt{op}}
+\newcommand\opPrime{\texttt{op'}}
+\newcommand\opSecond{\texttt{op''}}
+\newcommand\phimapping{\texttt{phi}}
+\newcommand\D{\texttt{D}}
+\newcommand\elt{\texttt{elt}}
+\newcommand\rel{\texttt{rel}}
+\newcommand\relp{\texttt{rel'}}
+
+%%%%%%%%%%%%%
+
+\begin{document}
+
+\begin{center}
+\begin{huge}
+Proposed naming conventions for the Coq standard library
+\end{huge}
+\end{center}
+\bigskip
+
+The following document describes a proposition of canonical naming
+schemes for the Coq standard library. Obviously and unfortunately, the
+current state of the library is not as homogeneous as it would be if
+it would systematically follow such a scheme. To tend in this
+direction, we however recommend to follow the following suggestions.
+
+\tableofcontents
+
+\section{General conventions}
+
+\subsection{Variable names}
+
+\begin{itemize}
+
+\item Variables are preferably quantified at the head of the
+  statement, even if some premisses do not depend of one of them. For
+  instance, one would state
+\begin{quote}
+\begin{tt}
+  {forall x y z:D, x <= y -> x+z <= y+z}
+\end{tt}
+\end{quote}
+and not
+\begin{quote}
+\begin{tt}
+  {forall x y:D, x <= y -> forall z:D, x+z <= y+z}
+\end{tt}
+\end{quote}
+
+\item Variables are preferably quantified (and named) in the order of
+  ``importance'', then of appearance, from left to right, even if
+  for the purpose of some tactics it would have been more convenient
+  to have, say, the variables not occurring in the conclusion
+  first. For instance, one would state
+\begin{quote}
+\begin{tt}
+  {forall x y z:D, x+z <= y+z -> x <= y}
+\end{tt}
+\end{quote}
+and not
+\begin{quote}
+\begin{tt}
+  {forall z x y:D, x+z <= y+z -> x <= y}
+\end{tt}
+\end{quote}
+nor
+\begin{quote}
+\begin{tt}
+  {forall x y z:D, y+x <= z+x -> y <= z}
+\end{tt}
+\end{quote}
+
+\item Choice of effective names is domain-dependent. For instance, on
+  natural numbers, the convention is to use the variables $n$, $m$,
+  $p$, $q$, $r$, $s$ in this order.
+
+  On generic domains, the convention is to use the letters $x$, $y$,
+  $z$, $t$. When more than three variables are needed, indexing variables
+
+  It is conventional to use specific names for variables having a
+  special meaning. For instance, $eps$ or $\epsilon$ can be used to
+  denote a number intended to be as small as possible. Also, $q$ and
+  $r$ can be used to denote a quotient and a rest. This is good
+  practice.
+
+\end{itemize}
+
+\subsection{Disjunctive statements}
+
+A disjunctive statement with a computational content will be suffixed
+by \name{\_inf}. For instance, if
+
+\begin{quote}
+\begin{tt}
+{forall x y, op x y = zero -> x = zero \/ y = zero}
+\end{tt}
+\end{quote}
+has name \texttt{D\_integral}, then
+\begin{quote}
+\begin{tt}
+{forall x y, op x y = zero -> \{x = zero\} + \{y = zero\}}
+\end{tt}
+\end{quote}
+will have name \texttt{D\_integral\_inf}.
+
+As an exception, decidability statements, such as 
+\begin{quote}
+\begin{tt}
+{forall x y, \{x = y\} + \{x <> y\}}
+\end{tt}
+\end{quote}
+will have a named ended in \texttt{\_dec}. Idem for cotransitivity
+lemmas which are inherently computational that are ended in
+\texttt{\_cotrans}.
+
+\subsection{Inductive types constructor names}
+
+As a general rule, constructor names start with the name of the
+inductive type being defined as in \texttt{Inductive Z := Z0 : Z |
+  Zpos : Z -> Z | Zneg : Z -> Z} to the exception of very standard
+types like \texttt{bool}, \texttt{nat}, \texttt{list}...
+
+For inductive predicates, constructor names also start with the name
+of the notion being defined with one or more suffixes separated with
+\texttt{\_} for discriminating the different cases as e.g. in
+
+\begin{verbatim}
+Inductive even : nat -> Prop :=
+  | even_O : even 0
+  | even_S n : odd n -> even (S n)
+with odd : nat -> Prop :=
+  | odd_S n : even n -> odd (S n).
+\end{verbatim}
+
+As a general rule, inductive predicate names should be lowercase (to
+the exception of notions referring to a proper name, e.g. \texttt{Bezout})
+and multiple words must be separated by ``{\_}''.
+
+As an exception, when extending libraries whose general rule is that
+predicates names start with a capital letter, the convention of this
+library should be kept and the separation between multiple words is
+done by making the initial of each work a capital letter (if one of
+these words is a proper name, then a ``{\_}'' is added to emphasize
+that the capital letter is proper and not an application of the rule
+for marking the change of word).
+
+Inductive predicates that characterize the specification of a function
+should be named after the function it specifies followed by
+\texttt{\_spec} as in:
+
+\begin{verbatim}
+Inductive nth_spec : list A -> nat -> A -> Prop :=
+  | nth_spec_O a l : nth_spec (a :: l) 0 a
+  | nth_spec_S n a b l : nth_spec l n a -> nth_spec (b :: l) (S n) a.
+\end{verbatim}
+
+\section{Equational properties of operations}
+
+\subsection{General conventions}
+
+If the conclusion is in the other way than listed below, add suffix
+\name{\_reverse} to the lemma name.
+
+\subsection{Specific conventions}
+
+\itemrule{Associativity of binary operator {\op} on domain {\D}}{Dop\_assoc}
+{forall x y z:D, op x (op y z) = op (op x y) z}
+
+  Remark: Symmetric form: \name{Dop\_assoc\_reverse}:
+  \formula{forall x y z:D, op (op x y) z = op x (op y z)}
+
+\itemrule{Commutativity of binary operator {\op} on domain {\D}}{Dop\_comm}
+{forall x y:D, op x y = op y x}
+
+  Remark: Avoid \formula{forall x y:D, op y x = op x y}, or at worst, call it
+  \name{Dop\_comm\_reverse}
+
+\itemrule{Left neutrality of element elt for binary operator {\op}}{Dop\_elt\_l}
+{forall x:D, op elt x = x}
+
+  Remark: In English, ``{\elt} is an identity for {\op}'' seems to be
+  a more common terminology.
+
+\itemrule{Right neutrality of element elt for binary operator {\op}}{Dop\_elt\_r}
+{forall x:D, op x elt = x}
+
+  Remark: By convention, if the identities are reminiscent to zero or one, they
+  are written 1 and 0 in the name of the property.
+
+\itemrule{Left absorption of element elt for binary operator {\op}}{Dop\_elt\_l}
+{forall x:D, op elt x = elt}
+
+  Remarks:
+  \begin{itemize}
+  \item In French school, this property is named "elt est absorbant pour op"
+  \item English, the property seems generally named "elt is a zero of op"
+  \item In the context of lattices, this a boundedness property, it may
+     be called "elt is a bound on D", or referring to a (possibly
+     arbitrarily oriented) order "elt is a least element of D" or "elt
+     is a greatest element of D"
+  \end{itemize}
+
+\itemrule{Right absorption of element {\elt} for binary operator {\op}}{Dop\_elt\_l  [BAD ??]}
+{forall x:D, op x elt = elt}
+
+\itemrule{Left distributivity of binary operator {\op} over {\opPrime} on domain {\D}}{Dop\_op'\_distr\_l}
+{forall x y z:D, op (op' x y) z = op' (op x z) (op y z)}
+
+  Remark: Some authors say ``distribution''.
+
+\itemrule{Right distributivity of binary operator {\op} over {\opPrime} on domain {\D}}{Dop\_op'\_distr\_r}
+{forall x y z:D, op z (op' x y) = op' (op z x) (op z y)}
+
+  Remark: Note the order of arguments.
+
+\itemrule{Distributivity of unary operator {\op} over binary op' on domain {\D}}{Dop\_op'\_distr}
+{forall x y:D, op (op' x y) = op' (op x) (op y)}
+
+\itemrule{Distributivity of unary operator {\op} over binary op' on domain {\D}}{Dop\_op'\_distr}
+{forall x y:D, op (op' x y) = op' (op x) (op y)}
+
+  Remark: For a non commutative operation with inversion of arguments, as in
+  \formula{forall x y z:D, op (op' x y) = op' (op y) (op y z)},
+  we may probably still call the property distributivity since there
+  is no ambiguity.
+
+  Example: \formula{forall n m : Z, -(n+m) = (-n)+(-m)}.
+
+  Example: \formula{forall l l' : list A, rev (l++l') = (rev l)++(rev l')}.
+
+\itemrule{Left extrusion of unary operator {\op} over binary op' on domain {\D}}{Dop\_op'\_distr\_l}
+{forall x y:D, op (op' x y) = op' (op x) y}
+
+  Question: Call it left commutativity ?? left swap ?
+
+\itemrule{Right extrusion of unary operator {\op} over binary op' on domain {\D}}{Dop\_op'\_distr\_r}
+{forall x y:D, op (op' x y) = op' x (op y)}
+
+\itemrule{Idempotency of binary operator {\op} on domain {\D}}{Dop\_idempotent}
+{forall x:D, op x n = x}
+
+\itemrule{Idempotency of unary operator {\op} on domain {\D}}{Dop\_idempotent}
+{forall x:D, op (op x) = op x}
+
+  Remark: This is actually idempotency of {\op} wrt to composition and
+  identity.
+
+\itemrule{Idempotency of element elt for binary operator {\op} on domain {\D}}{Dop\_elt\_idempotent}
+{op elt elt = elt}
+
+  Remark: Generally useless in CIC for concrete, computable operators
+
+  Remark: The general definition is ``exists n, iter n op x = x''.
+
+\itemrule{Nilpotency of element elt wrt a ring D with additive neutral
+element {\zero} and multiplicative binary operator
+{\op}}{Delt\_nilpotent} 
+{op elt elt = zero}
+
+  Remark: We leave the ring structure of D implicit; the general definition is ``exists n, iter n op elt = zero''.
+
+\itemrule{Zero-product property in a ring D with additive neutral
+element {\zero} and multiplicative binary operator
+{\op}}{D\_integral}
+{forall x y, op x y = zero -> x = zero \/ y = zero}
+
+  Remark: We leave the ring structure of D implicit; the Coq library
+  uses either \texttt{\_is\_O} (for \texttt{nat}), \texttt{\_integral}
+    (for \texttt{Z}, \texttt{Q} and \texttt{R}), \texttt{eq\_mul\_0} (for
+    \texttt{NZ}).
+
+  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}
+
+  Remark: Did not find this definition on the web, but it used in
+  the Coq library (to characterize \name{xor}).
+
+\itemrule{Involutivity of unary op on D}{Dop\_involutive}
+{forall x:D, op (op x) = x}
+
+\itemrule{Absorption law on the left for binary operator {\op} over binary operator {\op}' on the left}{Dop\_op'\_absorption\_l\_l}
+{forall x y:D, op x (op' x y) = x}
+
+\itemrule{Absorption law on the left for binary operator {\op} over binary operator {\op}' on the right}{Dop\_op'\_absorption\_l\_r}
+{forall x y:D, op x (op' y x) = x}
+
+  Remark: Similarly for \name{Dop\_op'\_absorption\_r\_l} and \name{Dop\_op'\_absorption\_r\_r}.
+
+\itemrule{De Morgan law's for binary operators {\opPrime} and {\opSecond} wrt
+to unary op on domain {\D}}{Dop'\_op''\_de\_morgan,
+Dop''\_op'\_de\_morgan ?? \mbox{leaving the complementing operation
+implicit})}
+{forall x y:D, op (op' x y) = op'' (op x) (op y)\\
+forall x y:D, op (op'' x y) = op' (op x) (op y)}
+
+\itemrule{Left complementation of binary operator {\op} by means of unary {\opPrime} wrt neutral element {\elt} of {\op} on domain {\D}}{Dop\_op'\_opp\_l}
+{forall x:D, op (op' x) x = elt}
+
+Remark: If the name of the opposite function is reminiscent of the
+notion of complement (e.g. if it is called \texttt{opp}), one can
+simply say {Dop\_opp\_l}.
+
+\itemrule{Right complementation of binary operator {\op} by means of unary {\op'} wrt neutral element {\elt} of {\op} on domain {\D}}{Dop\_opp\_r}
+{forall x:D, op x (op' x) = elt}
+
+Example: \formula{Radd\_opp\_l: forall r : R, - r + r = 0}
+
+\itemrule{Associativity of binary operators {\op} and {\op'}}{Dop\_op'\_assoc}
+{forall x y z, op x (op' y z) = op (op' x y) z}
+
+Example: \formula{forall x y z, x + (y - z) = (x + y) - z}
+
+\itemrule{Right extrusion of binary operator {\opPrime} over binary operator {\op}}{Dop\_op'\_extrusion\_r}
+{forall x y z, op x (op' y z) = op' (op x y) z}
+
+Remark: This requires {\op} and {\opPrime} to have their right and left
+argument respectively and their return types identical.
+
+Example: \formula{forall x y z, x + (y - z) = (x + y) - z}
+
+Remark: Other less natural combinations are possible, such
+as \formula{forall x y z, op x (op' y z) = op' y (op x z)}.
+
+\itemrule{Left extrusion of binary operator {\opPrime} over binary operator {\op}}{Dop\_op'\_extrusion\_l}
+{forall x y z, op (op' x y) z = op' x (op y z)}
+
+Remark: Operations are not necessarily internal composition laws.  It
+is only required that {\op} and {\opPrime} have their right and left
+argument respectively and their return type identical.
+
+Remark: When the type are heterogeneous, only one extrusion law is possible and it can simply be named {Dop\_op'\_extrusion}.
+
+Example: \formula{app\_cons\_extrusion : forall a l l', (a :: l) ++ l' = a :: (l ++ l')}.
+
+%======================================================================
+%\section{Properties of elements}
+
+%Remark: Not used in current library
+
+
+
+%======================================================================
+\section{Preservation and compatibility properties of operations}
+
+\subsection{With respect to equality}
+
+\itemrule{Injectivity of unary operator {\op}}{Dop\_inj}
+{forall x y:D, op x = op y -> x = y}
+
+\itemrule{Left regularity of binary operator {\op}}{Dop\_reg\_l, Dop\_inj\_l, or Dop\_cancel\_l}
+{forall x y z:D, op z x = op z y -> x = y}
+
+  Remark: Note the order of arguments.
+
+  Remark: The Coq usage is to called it regularity but the English
+  standard seems to be cancellation. The recommended form is not
+  decided yet.
+
+  Remark: Shall a property like $n^p \leq n^q \rightarrow p \leq q$
+  (for $n\geq 1$) be called cancellation or should it be reserved for
+  operators that have an inverse?
+
+\itemrule{Right regularity of binary operator {\op}}{Dop\_reg\_r, Dop\_inj\_r, Dop\_cancel\_r}
+{forall x y z:D, op x z = op y z -> x = y}
+
+\subsection{With respect to a relation {\rel}}
+
+\itemrule{Compatibility of unary operator {\op}}{Dop\_rel\_compat}
+{forall x y:D, rel x y -> rel (op x) (op y)}
+
+\itemrule{Left compatibility of binary operator {\op}}{Dop\_rel\_compat\_l}
+{forall x y z:D, rel x y -> rel (op z x) (op z y)}
+
+\itemrule{Right compatibility of binary operator {\op}}{Dop\_rel\_compat\_r}
+{forall x y z:D, rel x y -> rel (op x z) (op y z)}
+
+  Remark: For equality, use names of the form \name{Dop\_eq\_compat\_l} or
+  \name{Dop\_eq\_compat\_r}
+(\formula{forall x y z:D, y = x -> op y z = op x z} and
+\formula{forall x y z:D, y = x -> op y z = op x z})
+
+  Remark: Should we admit (or even prefer) the name
+  \name{Dop\_rel\_monotone}, \name{Dop\_rel\_monotone\_l},
+  \name{Dop\_rel\_monotone\_r} when {\rel} is an order ?
+
+\itemrule{Left regularity of binary operator {\op}}{Dop\_rel\_reg\_l}
+{forall x y z:D, rel (op z x) (op z y) -> rel x y}
+
+\itemrule{Right regularity of binary operator {\op}}{Dop\_rel\_reg\_r}
+{forall x y z:D, rel (op x z) (op y z) -> rel x y}
+
+  Question: Would it be better to have \name{z} as first argument, since it
+  is missing in the conclusion ?? (or admit we shall use the options
+  ``\texttt{with p}''?)
+
+\itemrule{Left distributivity of binary operator {\op} over {\opPrime} along relation {\rel} on domain {\D}}{Dop\_op'\_rel\_distr\_l}
+{forall x y z:D, rel (op (op' x y) z) (op' (op x z) (op y z))}
+
+  Example: standard property of (not necessarily distributive) lattices
+
+  Remark: In a (non distributive) lattice, by swapping join and meet,
+  one would like also,
+\formula{forall x y z:D, rel (op' (op x z) (op y z)) (op (op' x y) z)}.
+  How to name it with a symmetric name (use
+ \name{Dop\_op'\_rel\_distr\_mon\_l} and
+ \name{Dop\_op'\_rel\_distr\_anti\_l})?
+
+\itemrule{Commutativity of binary operator {\op} along (equivalence) relation {\rel} on domain {\D}}{Dop\_op'\_rel\_comm}
+{forall x y z:D, rel (op x y) (op y x)}
+
+  Example:
+\formula{forall l l':list A, Permutation (l++l') (l'++l)}
+
+\itemrule{Irreducibility of binary operator {\op} on domain {\D}}{Dop\_irreducible}
+{forall x y z:D, z = op x y -> z = x $\backslash/$ z = y}
+
+  Question: What about the constructive version ? Call it \name{Dop\_irreducible\_inf} ?
+\formula{forall x y z:D, z = op x y -> \{z = x\} + \{z = y\}}
+
+\itemrule{Primality of binary operator {\op} along relation {\rel} on domain {\D}}{Dop\_rel\_prime}
+{forall x y z:D, rel z (op x y) -> rel z x $\backslash/$ rel  z y}
+
+
+%======================================================================
+\section{Morphisms}
+
+\itemrule{Morphism between structures {\D} and {\D'}}{\name{D'\_of\_D}}{D -> D'}
+
+Remark: If the domains are one-letter long, one can used \texttt{IDD'} as for
+\name{INR} or \name{INZ}.
+
+\itemrule{Morphism {\phimapping} mapping unary operators {\op} to {\op'}}{phi\_op\_op', phi\_op\_op'\_morphism}
+{forall x:D, phi (op x) = op' (phi x)}
+
+Remark: If the operators have the same name in both domains, one use
+\texttt{D'\_of\_D\_op} or \texttt{IDD'\_op}.
+
+Example: \formula{Z\_of\_nat\_mult: forall n m : nat, Z\_of\_nat (n * m) = (Z\_of\_nat n * Z\_of\_nat m)\%Z}.
+
+Remark: If the operators have different names on distinct domains, one
+can use \texttt{op\_op'}.
+
+\itemrule{Morphism {\phimapping} mapping binary operators {\op} to
+{\op'}}{phi\_op\_op', phi\_op\_op'\_morphism}  {forall
+x y:D, phi (op x y) = op' (phi x) (phi y)}
+
+Remark: If the operators have the same name in both domains, one use
+\texttt{D'\_of\_D\_op} or \texttt{IDD'\_op}.
+
+Remark: If the operators have different names on distinct domains, one
+can use \texttt{op\_op'}.
+
+\itemrule{Morphism {\phimapping} mapping binary operator {\op} to
+binary relation {\rel}}{phi\_op\_rel, phi\_op\_rel\_morphism}
+{forall x y:D, phi (op x y) <-> rel (phi x) (phi y)}
+
+Remark: If the operator and the relation have similar name, one uses
+\texttt{phi\_op}. 
+
+Question: How to name each direction? (add \_elim for -> and \_intro
+for <- ?? -- as done in Bool.v ??)
+
+Example: \formula{eq\_true\_neg: \~{} eq\_true b <-> eq\_true (negb b)}.
+
+%======================================================================
+\section{Preservation and compatibility properties of operations wrt order}
+
+\itemrule{Compatibility of binary operator {\op} wrt (strict order) {\rel} and (large order) {\rel'}}{Dop\_rel\_rel'\_compat}
+{forall x y z t:D, rel x y -> rel' z t -> rel (op x z) (op y t)}
+
+\itemrule{Compatibility of binary operator {\op} wrt (large order) {\relp} and (strict order) {\rel}}{Dop\_rel'\_rel\_compat}
+{forall x y z t:D, rel' x y -> rel z t -> rel (op x z) (op y t)}
+
+
+%======================================================================
+\section{Properties of relations}
+
+\itemrule{Reflexivity of relation {\rel} on domain {\D}}{Drel\_refl}
+{forall x:D, rel x x}
+
+\itemrule{Symmetry of relation {\rel} on domain {\D}}{Drel\_sym}
+{forall x y:D, rel x y -> rel y x}
+
+\itemrule{Transitivity of relation {\rel} on domain {\D}}{Drel\_trans}
+{forall x y z:D, rel x y -> rel y z -> rel x z}
+
+\itemrule{Antisymmetry of relation {\rel} on domain {\D}}{Drel\_antisym}
+{forall x y:D, rel x y -> rel y x -> x = y}
+
+\itemrule{Irreflexivity of relation {\rel} on domain {\D}}{Drel\_irrefl}
+{forall x:D, \~{} rel x x}
+
+\itemrule{Asymmetry of relation {\rel} on domain {\D}}{Drel\_asym}
+{forall x y:D, rel x y -> \~{} rel y x}
+
+\itemrule{Cotransitivity of relation {\rel} on domain {\D}}{Drel\_cotrans}
+{forall x y z:D, rel x y -> \{rel z y\} + \{rel x z\}}
+
+\itemrule{Linearity of relation {\rel} on domain {\D}}{Drel\_trichotomy}
+{forall x y:D, \{rel x y\} + \{x = y\} + \{rel y x\}}
+
+  Questions: Or call it \name{Drel\_total}, or \name{Drel\_linear}, or
+  \name{Drel\_connected}? Use
+  $\backslash/$ ? or use a ternary sumbool, or a ternary disjunction,
+  for nicer elimination.
+
+\itemrule{Informative decidability of relation {\rel} on domain {\D}}{Drel\_dec (or Drel\_dect, Drel\_dec\_inf ?)}
+{forall x y:D, \{rel x y\} + \{\~{} rel x y\}}
+
+  Remark: If equality: \name{D\_eq\_dec} or \name{D\_dec} (not like
+  \name{eq\_nat\_dec})
+
+\itemrule{Non informative decidability of relation {\rel} on domain {\D}}{Drel\_dec\_prop (or Drel\_dec)}
+{forall x y:D, rel x y $\backslash/$ \~{} rel x y}
+
+\itemrule{Inclusion of relation {\rel} in relation {\rel}' on domain {\D}}{Drel\_rel'\_incl (or Drel\_incl\_rel')}
+{forall x y:D, rel x y -> rel' x y}
+
+  Remark: Use \name{Drel\_rel'\_weak} for a strict inclusion ??
+
+%======================================================================
+\section{Relations between properties}
+
+\itemrule{Equivalence of properties \texttt{P} and \texttt{Q}}{P\_Q\_iff}
+{forall x1 .. xn, P <-> Q}
+
+  Remark: Alternatively use \name{P\_iff\_Q} if it is too difficult to
+  recover what pertains to \texttt{P} and what pertains to \texttt{Q}
+  in their concatenation (as e.g. in
+  \texttt{Godel\_Dummett\_iff\_right\_distr\_implication\_over\_disjunction}).
+
+%======================================================================
+\section{Arithmetical conventions}
+
+\begin{minipage}{6in}
+\renewcommand{\thefootnote}{\thempfootnote}  % For footnotes...
+\begin{tabular}{lll}
+Zero on domain {\D} & D0 & (notation \verb=0=)\\
+One on domain {\D} & D1 (if explicitly defined) & (notation \verb=1=)\\
+Successor on domain {\D} & Dsucc\\
+Predessor on domain {\D} & Dpred\\
+Addition on domain {\D} & Dadd/Dplus\footnote{Coq historically uses \texttt{plus} and \texttt{mult} for addition and multiplication which are inconsistent notations, the recommendation is to use \texttt{add} and \texttt{mul} except in existng libraries that already use \texttt{plus} and \texttt{mult}}
+ & (infix notation \verb=+= [50,L])\\
+Multiplication on domain {\D} & Dmul/Dmult\footnotemark[\value{footnote}] & (infix notation \verb=*= [40,L]))\\
+Soustraction on domain {\D} & Dminus & (infix notation \verb=-= [50,L])\\
+Opposite on domain {\D} & Dopp (if any) & (prefix notation \verb=-= [35,R]))\\
+Inverse on domain {\D} & Dinv (if any) & (prefix notation \verb=/= [35,R]))\\
+Power on domain {\D} & Dpower & (infix notation \verb=^= [30,R])\\
+Minimal element on domain {\D} & Dmin\\
+Maximal element on domain {\D} & Dmax\\
+Large less than order on {\D} & Dle & (infix notations \verb!<=! and \verb!>=! [70,N]))\\
+Strict less than order on {\D} & Dlt & (infix notations \verb=<= and \verb=>= [70,N]))\\
+\end{tabular}
+\bigskip
+\end{minipage}
+
+\bigskip
+
+The status of \verb!>=! and \verb!>! is undecided yet. It will eithet
+be accepted only as parsing notations or may also accepted as a {\em
+  definition} for the \verb!<=! and \verb!<! (like in \texttt{nat}) or
+even as a different definition (like it is the case in \texttt{Z}).
+
+\bigskip
+
+Exception: Peano Arithmetic which is used for pedagogical purpose:
+
+\begin{itemize}
+\item domain name is implicit
+\item \term{0} (digit $0$) is \term{O} (the 15th letter of the alphabet)
+\item \term{succ} is \verb!S! (but \term{succ} can be used in theorems)
+\end{itemize}
+
+\end{document}
diff --git a/dev/doc/patch.ocaml-3.10.drop.rectypes b/dev/doc/patch.ocaml-3.10.drop.rectypes
new file mode 100644
index 00000000..ba7a3e95
--- /dev/null
+++ b/dev/doc/patch.ocaml-3.10.drop.rectypes
@@ -0,0 +1,31 @@
+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/perf-analysis b/dev/doc/perf-analysis
index 8e481544..d23bf835 100644
--- a/dev/doc/perf-analysis
+++ b/dev/doc/perf-analysis
@@ -1,6 +1,14 @@
 Performance analysis (trunk repository)
 ---------------------------------------
 
+Dec 1, 2009 - Dec 19, 2009: Temporary addition of [forall x, P x] hints to
+  exact (generally not significative but, e.g., +25% on Subst, +8% on
+  ZFC, +5% on AreaMethod)
+
+Oct 19, 2009: Change in modules (CoLoR +35%)
+
+Aug 9, 2009: new files added in AreaMethod 
+
 May 21, 2008: New version of CoRN
   (needs +84% more time to compile)
 
diff --git a/dev/doc/versions-history.tex b/dev/doc/versions-history.tex
new file mode 100644
index 00000000..175297f9
--- /dev/null
+++ b/dev/doc/versions-history.tex
@@ -0,0 +1,351 @@
+\documentclass[a4paper]{book}
+\usepackage{fullpage}
+\usepackage[latin1]{inputenc}
+\usepackage[T1]{fontenc}
+\usepackage{amsfonts}
+
+\newcommand{\feature}[1]{{\em #1}}
+
+\begin{document}
+
+\begin{center}
+\begin{huge}
+An history of Coq versions
+\end{huge}
+\end{center}
+\bigskip
+
+\centerline{\large 1984-1989: The Calculus of Constructions}
+\mbox{}\\
+\mbox{}\\
+\begin{tabular}{l|l|l}
+version & date & comments \\
+\hline
+CoC V1.10& mention of dates from 6 December & implementation language is Caml\\
+         & 1984 to 13 February 1985 \\
+
+CoC V1.11& mention of dates from 6 December\\
+         & 1984 to 19 February 1985\\
+
+CoC V2.13& dated 16 December 1985\\
+
+CoC V2.13& dated 25 June 1986\\
+
+CoC V3.1& dated 20 November 1986 & \feature{auto}\\
+
+CoC V3.2& dated 27 November 1986\\
+
+CoC V3.3 and V3.4& dated 1 January 1987 & creation of a directory for examples\\
+
+CoC V4.1& dated 24 July 1987\\
+
+CoC V4.2& dated 10 September 1987\\
+
+CoC V4.3& dated 15 September 1987\\
+
+CoC V4.4& dated 27 January 1988\\
+
+CoC V4.5 and V4.5.5& dated 15 March 1988\\
+
+CoC V4.6 and V4.7& dated 1 September 1988\\
+
+CoC V4.8& dated 1 December 1988\\
+
+CoC V4.8.5& dated 1 February 1989\\
+
+CoC V4.9& dated 1 March 1989\\
+
+CoC V4.10 and 4.10.1& dated 1 May 1989 & first public release - in English\\
+\end{tabular}
+
+\bigskip
+\bigskip
+
+\newpage
+
+\centerline{\large 1989-now: The Calculus of Inductive Constructions}
+\mbox{}\\
+\centerline{I- RCS archives in Caml and Caml-Light}
+\mbox{}\\
+\mbox{}\\
+\begin{tabular}{l|l|l}
+version & date & comments \\
+\hline
+Coq V5.0 & headers dated 1 January 1990 & internal use \\
+  & & \feature{inductive types with primitive recursor}\\
+
+Coq V5.1 & ended 12 July 1990 & internal use \\
+
+Coq V5.2 & log dated 4 October 1990 & internal use \\
+
+Coq V5.3 & log dated 12 October 1990 & internal use \\
+
+Coq V5.4 & headers dated 24 October 1990 & internal use, \feature{extraction} (version 1) [3-12-90]\\
+
+Coq V5.5 & started 6 December 1990 & internal use \\
+
+Coq V5.6 beta & 1991 & first announce of the new Coq based on CIC \\
+ & & (in May at TYPES?)\\
+ & & \feature{rewrite tactic}\\
+ & & use of RCS at least from February 1991\\
+
+Coq V5.6& 7 August 1991 & \\
+
+Coq V5.6 patch 1& 13 November 1991 & \\
+
+Coq V5.6 (last) & mention of 27 November 1992\\
+
+Coq V5.7.0& 1992 & translation to Caml-Light \footnotemark\\
+
+Coq V5.8& 12 February 1993 & \feature{Program} (version 1), \feature{simpl}\\
+
+& & has the xcoq graphical interface\\
+
+& & first explicit notion of standard library\\
+
+& & includes a MacOS 7-9 version\\
+
+Coq V5.8.1& released 28 April 1993 & with xcoq graphical interface and MacOS 7-9 support\\
+
+Coq V5.8.2& released 9 July 1993 & with xcoq graphical interface and MacOS 7-9 support\\
+
+Coq V5.8.3& released 6 December 1993 % Announce on coq-club
+          & with xcoq graphical interface and MacOS 7-9 support\\
+
+ & & 3 branches: Lyon (V5.8.x), Ulm (V5.10.x) and Rocq (V5.9)\\
+
+Coq V5.9 alpha& 7 July 1993 & 
+experimental version based on evars refinement \\
+              & & (merge from experimental ``V6.0'' and some pre-V5.8.3 \\
+              & & version), not released\\
+
+& March 1994 & \feature{tauto} tactic in V5.9 branch\\
+
+Coq V5.9 & 27 January 1993 & experimental version based on evars refinement\\
+         & & not released\\
+\end{tabular}
+
+\bigskip
+\bigskip
+
+\footnotetext{archive lost?}
+
+\newpage
+
+\centerline{II- Starting with CVS archives in Caml-Light}
+\mbox{}\\
+\mbox{}\\
+\begin{tabular}{l|l|l}
+version & date & comments \\
+\hline
+Coq V5.10 ``Murthy'' & 22 January 1994 & 
+introduction of the ``DOPN'' structure\\
+ & & \feature{eapply/prolog} tactics\\
+ & & private use of cvs on madiran.inria.fr\\
+
+Coq V5.10.1 ``Murthy''& 15 April 1994 \\
+
+Coq V5.10.2 ``Murthy''& 19 April 1994 & \feature{mutual inductive types, fixpoint} (from Lyon's branch)\\
+
+Coq V5.10.3& 28 April 1994 \\
+
+Coq V5.10.5& dated 13 May 1994 & \feature{inversion}, \feature{discriminate}, \feature{injection} \\
+  & & \feature{type synthesis of hidden arguments}\\
+  & & \feature{separate compilation}, \feature{reset mechanism} \\
+
+Coq V5.10.6& dated 30 May 1994\\
+Coq Lyon's archive & in 1994 & cvs server set up on woodstock.ens-lyon.fr\\
+
+Coq V5.10.9& announced on 17 August 1994 &
+ % Announced by Catherine Parent on coqdev
+ % Version avec une copie de THEORIES pour les inductifs mutuels 
+ \\
+
+Coq V5.10.11& announced on 2 February 1995 & \feature{compute}\\
+Coq Rocq's archive & on 16 February 1995 & set up of ``V5.10'' cvs archive on pauillac.inria.fr \\
+ & & with first dispatch of files over src/* directories\\
+
+Coq V5.10.12& dated 30 January 1995 & on Lyon's cvs\\
+
+Coq V5.10.13& dated 9 June 1995 & on Lyon's cvs\\
+
+Coq V5.10.14.OO& dated 30 June 1995 & on Lyon's cvs\\
+
+Coq V5.10.14.a& announced 5 September 1995 & bug-fix release \\ % Announce on coq-club by BW 
+
+Coq V5.10.14.b& released 2 October 1995 & bug-fix release\\
+  & & MS-DOS version released on 30 October 1995\\
+ % still available at ftp://ftp.ens-lyon.fr/pub/LIP/COQ/V5.10.14.old/ in May 2009
+ % also known in /net/pauillac/constr archive as ``V5.11 old'' \\
+ % A copy of Coq V5.10.15 dated 1 January 1996 coming from Lyon's CVS is
+ % known in /net/pauillac/constr archive as ``V5.11 new old'' \\
+
+Coq V5.10.15 & released 20 February 1996 & \feature{Logic, Sorting, new Sets and Relations libraries} \\
+  % Announce on coq-club by BW
+  % dated 15 February 1996 and bound to pauillac's cvs in /net/pauillac/constr archive 
+  & & MacOS 7-9 version released on 1 March 1996 \\ % Announce on coq-club by BW
+
+Coq V5.11 & dated 1 March 1996 & not released, not in pauillac's CVS, \feature{eauto} \\
+\end{tabular}
+
+\bigskip
+\bigskip
+
+\newpage
+
+\centerline{III- A CVS archive in Caml Special Light}
+\mbox{}\\
+\mbox{}\\
+\begin{tabular}{l|l|l}
+version & date & comments \\
+\hline
+Coq ``V6'' archive & 20 March 1996 & new cvs repository on pauillac.inria.fr with code ported \\
+ & & to Caml Special Light (to later become Objective Caml)\\
+ & & has implicit arguments and coercions\\
+
+Coq V6.1beta& released 18 November 1996 & \feature{coercions} [23-5-1996], \feature{user-level implicit arguments} [23-5-1996]\\
+ & & \feature{omega} [10-9-1996] \\
+ & & \feature{natural language proof printing} (stopped from Coq V7) [6-9-1996]\\
+ & & \feature{pattern-matching compilation} [7-10-1996]\\
+ & & \feature{ring} (version 1, ACSimpl) [11-12-1996]\\
+
+Coq V6.1& released December 1996 & \\
+
+Coq V6.2beta& released 30 January 1998 & % Announced on coq-club 2-2-1998 by CP
+      \feature{SearchIsos} (stopped from Coq V7) [9-11-1997]\\
+  & & grammar extension mechanism moved to Camlp4 [12-6-1997]\\
+  & & \feature{refine tactic}\\
+  & & includes a Windows version\\
+
+Coq V6.2& released 4 May 1998 & % Announced on coq-club 5-5-1998 by CP
+  \feature{ring} (version 2) [7-4-1998] \\
+
+Coq V6.2.1& released 23 July 1998\\
+
+Coq V6.2.2 beta& released 30 January 1998\\
+
+Coq V6.2.2& released 23 September 1998\\
+
+Coq V6.2.3& released 22 December 1998 & \feature{Real numbers library} [from 13-11-1998] \\
+
+Coq V6.2.4& released 8 February 1999\\
+
+Coq V6.3& released 27 July 1999 & \feature{autorewrite} [25-3-1999]\\
+ & & \feature{Correctness} (deprecated in V8, led to Why) [28-10-1997]\\
+
+Coq V6.3.1& released 7 December 1999\\
+\end{tabular}
+\medskip
+\bigskip
+
+\newpage
+\centerline{IV- New CVS, back to a kernel-centric implementation}
+\mbox{}\\
+\mbox{}\\
+\begin{tabular}{l|l|l}
+version & date & comments \\
+\hline
+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)\\
+Coq V7.0beta& released 27 December 2000 & \feature{${\cal L}_{\mathit{tac}}$} \\
+Coq V7.0beta2& released 2 February 2001\\
+
+Coq V7.0& released 25 April 2001 & \feature{extraction} (version 2) [6-2-2001] \\
+  & & \feature{field} (version 1) [19-4-2001], \feature{fourier} [20-4-2001] \\
+
+Coq V7.1& released 25 September 2001 & \feature{setoid rewriting} (version 1) [10-7-2001]\\
+
+Coq V7.2& released 10 January 2002\\
+
+Coq V7.3& released 16 May 2002\\
+
+Coq V7.3.1& released 5 October 2002 & \feature{module system} [2-8-2002]\\
+  & & \feature{pattern-matching compilation} (version 2) [13-6-2002]\\
+
+Coq V7.4& released 6 February 2003 & \feature{notation}, \feature{scopes} [13-10-2002]\\
+
+Coq V8.0& released 21 April 2004 & \feature{new concrete syntax}, \feature{Set predicative}, \feature{CoqIDE} [from 4-2-2003]\\
+
+Coq V8.0pl1& released 18 July 2004\\
+
+Coq V8.0pl2& released 22 January 2005\\
+
+Coq V8.0pl3& released 13 January 2006\\
+
+Coq V8.0pl4& released 26 January 2007\\
+
+Coq ``svn'' archive & 6 March 2006 & cvs archive moved to subversion control management\\
+
+Coq V8.1beta& released 12 July 2006 & \feature{bytecode compiler} [20-10-2004] \\
+  & & \feature{setoid rewriting} (version 2) [3-9-2004]\\
+  & & \feature{functional induction} [1-2-2006]\\
+  & & \feature{Strings library} [8-2-2006], \feature{FSets/FMaps library} [15-3-2006] \\
+  & & \feature{Program} (version 2, Russell) [5-3-2006] \\
+  & & \feature{declarative language} [20-9-2006]\\
+  & & \feature{ring} (version 3) [18-11-2005]\\
+
+Coq V8.1gamma& released 7 November 2006 & \feature{field} (version 2) [29-9-2006]\\
+
+Coq V8.1& released 10 February 2007 & \\
+
+Coq V8.1pl1& released 27 July 2007 & \\
+Coq V8.1pl2& released 13 October 2007 & \\
+Coq V8.1pl3& released 13 December 2007 & \\
+Coq V8.1pl4& released 9 October 2008 & \\
+
+Coq V8.2 beta1& released 13 June 2008 & \\
+Coq V8.2 beta2& released 19 June 2008 & \\
+Coq V8.2 beta3& released 27 June 2008 & \\
+Coq V8.2 beta4& released 8 August 2008 & \\
+
+Coq V8.2 & released 17 February 2009 & \feature{type classes} [10-12-2007], \feature{machine words} [11-5-2007]\\
+  & & \feature{big integers} [11-5-2007], \feature{abstract arithmetics} [9-2007]\\
+  & & \feature{setoid rewriting} (version 3) [18-12-2007] \\
+  & & \feature{micromega solving platform} [19-5-2008]\\
+
+& & a first package released on
+February 11 was incomplete\\
+\end{tabular}
+
+\medskip
+\bigskip
+\newpage
+
+\centerline{\large Other important dates}
+\mbox{}\\
+\mbox{}\\
+\begin{tabular}{l|l|l}
+version & date & comments \\
+\hline
+Lechenadec's version in C& mention of \\
+ & 13 January 1985 on \\
+ & some vernacular files\\
+Set up of the coq-club mailing list & 28 July 1993\\
+
+Coq V6.0 ``evars'' & & experimentation based on evars
+refinement started \\
+  & & in 1991 by Gilles from V5.6 beta,\\
+  & & with work by Hugo in July 1992\\
+
+Coq V6.0 ``evars'' ``light'' & July 1993 & Hugo's port of the first
+evars-based experimentation \\
+ & & to Coq V5.7, version from October/November
+1992\\
+
+CtCoq & released 25 October 1995 & first beta-version  \\ % Announce on coq-club by Janet  
+
+Proto with explicit substitutions & 1997 &\\
+
+Coq web site & 15 April 1998 & new site designed by David Delahaye \\
+
+Coq web site & January 2004 & web site new style \\
+  & & designed by Julien Narboux and Florent Kirchner \\
+
+Coq web site & April 2009 & new Drupal-based site \\
+  & & designed by Jean-Marc Notin and Denis Cousineau \\
+
+\end{tabular}
+
+\end{document}
diff --git a/dev/include b/dev/include
index ccb75edd..251a969b 100644
--- a/dev/include
+++ b/dev/include
@@ -1,12 +1,13 @@
 
 (* File to include to install the pretty-printers in the ocaml toplevel *)
 
-(* clflags.cmi (a ocaml compilation by-product) must be in the library path.
+(* For OCaml 3.10.x:
+   clflags.cmi (a ocaml compilation by-product) must be in the library path.
    On Debian, install ocaml-compiler-libs, and uncomment the following:
    #directory "+compiler-libs/utils";;
+   Clflags.recursive_types := true;;
 *)
 
-(* Clflags.recursive_types := true;;*)
 #cd ".";;
 #use "base_include";;
 
@@ -22,12 +23,13 @@
 #install_printer  (* type_judgement *) pptype;;
 #install_printer  (* judgement *) ppj;;
 
+#install_printer  (* hint_db *)  print_hint_db;;
 #install_printer  (* goal *)  ppgoal;;
 #install_printer  (* sigma goal *)  ppsigmagoal;;
 #install_printer  (* proof *)  pproof;;
+#install_printer  (* pftreestate *)  pppftreestate;;
 #install_printer  (* metaset.t *) ppmetas;;
 #install_printer  (* evar_map *)  ppevm;;
-#install_printer  (* evar_defs *)  ppevd;;
 #install_printer  (* clenv *) ppclenv;;
 #install_printer  (* env *) ppenv;;
 
@@ -37,4 +39,3 @@
 #install_printer  (* generic_argument *) pp_generic_argument;;
 
 #install_printer  (* fconstr *) ppfconstr;;
-
diff --git a/dev/ocamldebug-coq.template b/dev/ocamldebug-coq.template
index 5f49561b..74320588 100644
--- a/dev/ocamldebug-coq.template
+++ b/dev/ocamldebug-coq.template
@@ -17,13 +17,15 @@ exec $OCAMLDEBUG \
 	-I $COQTOP/library -I $COQTOP/pretyping -I $COQTOP/parsing \
         -I $COQTOP/interp -I $COQTOP/proofs -I $COQTOP/tactics \
 	-I $COQTOP/toplevel -I $COQTOP/dev -I $COQTOP/config \
-        -I $COQTOP/contrib/extraction -I $COQTOP/contrib/field \
-        -I $COQTOP/contrib/fourier    -I $COQTOP/contrib/firstorder \
-        -I $COQTOP/contrib/interface  -I $COQTOP/contrib/cc \
-        -I $COQTOP/contrib/omega      -I $COQTOP/contrib/romega \
-        -I $COQTOP/contrib/ring       -I $COQTOP/contrib/xml \
-	-I $COQTOP/contrib/subtac     -I $COQTOP/contrib/funind \
-        -I $COQTOP/contrib/rtauto     -I $COQTOP/contrib/setoid_ring \
-        -I $COQTOP/contrib/recdef     -I $COQTOP/contrib/dp \
+        -I $COQTOP/plugins/cc         -I $COQTOP/plugins/dp \
+        -I $COQTOP/plugins/extraction -I $COQTOP/plugins/field \
+        -I $COQTOP/plugins/firstorder -I $COQTOP/plugins/fourier \
+        -I $COQTOP/plugins/funind     -I $COQTOP/plugins/groebner \
+        -I $COQTOP/plugins/interface  -I $COQTOP/plugins/micromega \
+        -I $COQTOP/plugins/omega      -I $COQTOP/plugins/quote \
+        -I $COQTOP/plugins/ring       -I $COQTOP/plugins/romega \
+	-I $COQTOP/plugins/rtauto     -I $COQTOP/plugins/setoid_ring \
+        -I $COQTOP/plugins/subtac     -I $COQTOP/plugins/syntax \
+        -I $COQTOP/plugins/xml \
         -I $COQTOP/ide \
 	$*
diff --git a/dev/ocamlopt_shared_os5fix.sh b/dev/ocamlopt_shared_os5fix.sh
new file mode 100755
index 00000000..f7d31ad8
--- /dev/null
+++ b/dev/ocamlopt_shared_os5fix.sh
@@ -0,0 +1,29 @@
+#/bin/sh
+
+### Temporary fix for production of .cmxs on MacOS 10.5
+
+OCAMLOPT=$1
+CMXS=$2
+
+DIR=`dirname $CMXS`
+BASE=`basename $CMXS .cmxs`
+CMXA=$DIR/$BASE.cmxa
+ARC=$DIR/$BASE.a
+# we assume that all object files are at the same place than the rest
+OBJS=`ar t $ARC | sed -e "s|^|$DIR/|" | grep -v SYMDEF`
+
+$OCAMLOPT -dstartup -linkall -shared -o $CMXS $CMXA
+# Fix1: add a dummy instruction before the caml generic functions
+# Fix2: make all caml generic functions private
+rm -f $CMXS $CMXS.startup.fixed.s
+cat $CMXS.startup.s | sed \
+ -e "s/_caml_shared_startup__code_begin:/_caml_shared_startup__code_begin:	ret/" \
+ -e "s/.globl	_caml_curry/.private_extern	_caml_curry/" \
+ -e "s/.globl	_caml_apply/.private_extern	_caml_apply/" \
+ -e "s/.globl	_caml_tuplify/.private_extern	_caml_tuplify/" \
+ > $CMXS.startup.fixed.s
+# Recompile fixed startup code
+as -o $CMXS.startup.o $CMXS.startup.fixed.s
+# Build fixed .cmxs (assume all object files are at the same place)
+ld -bundle -flat_namespace -undefined warning -read_only_relocs suppress -o $CMXS $OBJS $CMXS.startup.o
+rm $CMXS.startup.o $CMXS.startup.s $CMXS.startup.fixed.s
\ No newline at end of file
diff --git a/dev/ocamlweb-doc/Makefile b/dev/ocamlweb-doc/Makefile
index f2c625ed..3189d7c5 100644
--- a/dev/ocamlweb-doc/Makefile
+++ b/dev/ocamlweb-doc/Makefile
@@ -4,14 +4,14 @@ LOCALINCLUDES=-I ../../config -I ../../tools -I ../../tools/coqdoc \
 	      -I ../../scripts -I ../../lib -I ../../kernel -I ../../kernel/byterun -I ../../library \
               -I ../../proofs -I ../../tactics -I ../../pretyping \
               -I ../../interp -I ../../toplevel -I ../../parsing -I ../../ide/utils -I ../../ide \
-              -I ../../contrib/omega -I ../../contrib/romega \
-	      -I ../../contrib/ring -I ../../contrib/dp -I ../../contrib/setoid_ring \
-              -I ../../contrib/xml -I ../../contrib/extraction \
-              -I ../../contrib/interface -I ../../contrib/fourier \
-	      -I ../../contrib/cc \
-	      -I ../../contrib/funind -I ../../contrib/firstorder \
-              -I ../../contrib/field -I ../../contrib/subtac -I ../../contrib/rtauto \
-              -I ../../contrib/recdef
+              -I ../../plugins/omega -I ../../plugins/romega \
+	      -I ../../plugins/ring -I ../../plugins/dp -I ../../plugins/setoid_ring \
+              -I ../../plugins/xml -I ../../plugins/extraction \
+              -I ../../plugins/fourier \
+	      -I ../../plugins/cc \
+	      -I ../../plugins/funind -I ../../plugins/firstorder \
+              -I ../../plugins/field -I ../../plugins/subtac -I ../../plugins/rtauto \
+              -I ../../plugins/recdef
 
 MLINCLUDES=$(LOCALINCLUDES) -I $(MYCAMLP4LIB)
 
diff --git a/dev/ocamlweb-doc/ast.ml b/dev/ocamlweb-doc/ast.ml
index 2153ef47..4eb135d8 100644
--- a/dev/ocamlweb-doc/ast.ml
+++ b/dev/ocamlweb-doc/ast.ml
@@ -22,7 +22,7 @@ type constr_ast =
       (string * binder list * constr_ast * string option * constr_ast) list *
       string
 | Match of case_item list * constr_ast option *
-           (pattern list * constr_ast) list 
+           (pattern list * constr_ast) list
 
 and red_fun = Simpl
 
@@ -34,7 +34,7 @@ and fix_kind = Fix | CoFix
 
 and case_item = constr_ast * (string option * constr_ast option)
 
-and pattern = 
+and pattern =
   PatAs of pattern * string
 | PatType of pattern * constr_ast
 | PatConstr of string * pattern list
diff --git a/dev/ocamlweb-doc/lex.mll b/dev/ocamlweb-doc/lex.mll
index 617163e7..059526d9 100644
--- a/dev/ocamlweb-doc/lex.mll
+++ b/dev/ocamlweb-doc/lex.mll
@@ -7,7 +7,7 @@
 
  let comment_depth = ref 0
  let print s = output_string !chan_out s
- 
+
  exception Fin_fichier
 
 }
@@ -77,5 +77,5 @@ and comment = parse
   | "(*" (*"*)"*)  { incr comment_depth; comment lexbuf }
   | (*"(*"*) "*)"
       { decr comment_depth; if !comment_depth > 0 then comment lexbuf }
-  | eof   { raise Fin_fichier } 
+  | eof   { raise Fin_fichier }
   | _     { comment lexbuf }
diff --git a/dev/ocamlweb-doc/parse.ml b/dev/ocamlweb-doc/parse.ml
index e537b1f2..b145fffd 100644
--- a/dev/ocamlweb-doc/parse.ml
+++ b/dev/ocamlweb-doc/parse.ml
@@ -82,7 +82,7 @@ let rec str_stack = function
   | Term (t,s) -> str_stack s ^ " (" ^ str_ast t ^ ")"
   | Oper(ops,lop,t,s) ->
       str_stack (Term(t,s)) ^ " " ^ lop ^ " " ^
-      String.concat " " (List.rev ops) 
+      String.concat " " (List.rev ops)
 
 let pps s = prerr_endline (str_stack s)
 let err s stk = failwith (s^": "^str_stack stk)
diff --git a/dev/printers.mllib b/dev/printers.mllib
new file mode 100644
index 00000000..e8ec10c5
--- /dev/null
+++ b/dev/printers.mllib
@@ -0,0 +1,133 @@
+Coq_config
+
+Pp_control
+Pp
+Compat
+Flags
+Segmenttree
+Unicodetable
+Util
+Bigint
+Hashcons
+Dyn
+System
+Envars
+Bstack
+Edit
+Gset
+Gmap
+Fset
+Fmap
+Tlm
+Gmapl
+Profile
+Explore
+Predicate
+Rtree
+Heap
+Option
+Dnet
+
+Names
+Univ
+Esubst
+Term
+Mod_subst
+Sign
+Cbytecodes
+Copcodes
+Cemitcodes
+Declarations
+Retroknowledge
+Pre_env
+Cbytegen
+Environ
+Conv_oracle
+Closure
+Reduction
+Type_errors
+Entries
+Modops
+Inductive
+Typeops
+Indtypes
+Cooking
+Term_typing
+Subtyping
+Mod_typing
+Safe_typing
+
+Summary
+Nameops
+Libnames
+Global
+Nametab
+Libobject
+Lib
+Goptions
+Decls
+Heads
+Termops
+Namegen
+Evd
+Rawterm
+Reductionops
+Inductiveops
+Retyping
+Cbv
+Pretype_errors
+Evarutil
+Term_dnet
+Recordops
+Evarconv
+Typing
+Pattern
+Matching
+Tacred
+Classops
+Typeclasses_errors
+Typeclasses
+Detyping
+Indrec
+Coercion
+Unification
+Cases
+Pretyping
+Clenv
+
+Lexer
+Ppextend
+Genarg
+Topconstr
+Notation
+Dumpglob
+Reserve
+Impargs
+Constrextern
+Syntax_def
+Implicit_quantifiers
+Smartlocate
+Constrintern
+Proof_trees
+Tacexpr
+Proof_type
+Logic
+Refiner
+Evar_refiner
+Pfedit
+Tactic_debug
+Decl_mode
+Ppconstr
+Extend
+Extrawit
+Pcoq
+Printer
+Pptactic
+Ppdecl_proof
+Tactic_printer
+Egrammar
+Himsg
+Cerrors
+Vernacexpr
+Vernacinterp
+Top_printers
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index d7d2f6d8..23701c23 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -28,10 +28,11 @@ open Cerrors
 open Evd
 open Goptions
 open Genarg
+open Mod_subst
 
 
 let _ = Constrextern.print_evar_arguments := true
-let _ = set_bool_option_value (SecondaryTable ("Printing","Matching")) false
+let _ = set_bool_option_value ["Printing";"Matching"] false
 let _ = Detyping.set_detype_anonymous (fun _ _ -> raise Not_found)
 
 (* std_ppcmds *)
@@ -40,13 +41,13 @@ let pppp x = pp x
 (* name printers *)
 let ppid id = pp (pr_id id)
 let pplab l = pp (pr_lab l)
-let ppmsid msid = pp (str (debug_string_of_msid msid))
 let ppmbid mbid = pp (str (debug_string_of_mbid mbid))
 let ppdir dir = pp (pr_dirpath dir)
 let ppmp mp = pp(str (string_of_mp mp))
-let ppcon con = pp(pr_con con)
+let ppcon con = pp(debug_pr_con con)
 let ppkn kn = pp(pr_kn kn)
-let ppsp sp = pp(pr_sp sp)
+let ppmind kn = pp(debug_pr_mind kn)
+let ppsp sp = pp(pr_path sp)
 let ppqualid qid = pp(pr_qualid qid)
 let ppclindex cl = pp(Classops.pr_cl_index cl)
 
@@ -65,17 +66,30 @@ let ppfconstr c = ppconstr (Closure.term_of_fconstr c)
 
 let ppbigint n = pp (Bigint.pr_bigint n);;
 
-let prset pr l = str "[" ++ prlist_with_sep spc pr l ++ str "]"
+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 prset' pr l = str "[" ++ hov 0 (prlist_with_sep pr_comma pr l) ++ str "]"
+let ppidmap 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 []))
+
+let ppevarsubst = ppidmap (fun id0 -> prset (fun (c,copt,id) ->
+  hov 0
+  (Termops.print_constr c ++
+   (match copt with None -> mt () | Some c -> spc () ++ str "<expanded: " ++
+    Termops.print_constr c ++ str">") ++
+   (if id = id0 then mt ()
+    else spc () ++ str "<canonical: " ++ pr_id id ++ str ">"))))
+
 let pP s = pp (hov 0 s)
 
-let safe_pr_global = function 
-  | ConstRef kn -> pp (str "CONSTREF(" ++ pr_con kn ++ str ")")
-  | IndRef (kn,i) -> pp (str "INDREF(" ++ pr_kn kn ++ str "," ++ 
+let safe_pr_global = function
+  | ConstRef kn -> pp (str "CONSTREF(" ++ debug_pr_con kn ++ str ")")
+  | IndRef (kn,i) -> pp (str "INDREF(" ++ debug_pr_mind kn ++ str "," ++
 			  int i ++ str ")")
-  | ConstructRef ((kn,i),j) -> pp (str "INDREF(" ++ pr_kn kn ++ str "," ++ 
+  | ConstructRef ((kn,i),j) -> pp (str "INDREF(" ++ debug_pr_mind kn ++ str "," ++
 				      int i ++ str "," ++ int j ++ str ")")
   | VarRef id -> pp (str "VARREF(" ++ pr_id id ++ str ")")
 
@@ -92,6 +106,7 @@ let genppj f j = let (c,t) = f j in (c ++ str " : " ++ t)
 let ppj j = pp (genppj pr_ljudge j)
 
 let prsubst s = pp (Mod_subst.debug_pr_subst s)
+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)
@@ -100,9 +115,9 @@ let pp_transparent_state s = pp (pr_transparent_state s)
 (* proof printers *)
 let ppmetas metas = pp(pr_metaset metas)
 let ppevm evd = pp(pr_evar_map evd)
-let ppevd evd = pp(pr_evar_defs evd)
 let ppclenv clenv = pp(pr_clenv clenv)
 let ppgoal g = pp(db_pr_goal g)
+let pppftreestate p = pp(print_pftreestate p)
 
 let pr_gls gls =
   hov 0 (pr_evar_map (sig_sig gls) ++ fnl () ++ db_pr_goal (sig_it gls))
@@ -134,7 +149,7 @@ let ppobj obj = Format.print_string (Libobject.object_tag obj)
 
 let cnt = ref 0
 
-let cast_kind_display k = 
+let cast_kind_display k =
   match k with
   | VMcast -> "VMcast"
   | DEFAULTcast -> "DEFAULTcast"
@@ -145,7 +160,7 @@ let constr_display csr =
   | Meta n -> "Meta("^(string_of_int n)^")"
   | Var id -> "Var("^(string_of_id id)^")"
   | Sort s -> "Sort("^(sort_display s)^")"
-  | Cast (c,k, t) -> 
+  | Cast (c,k, t) ->
       "Cast("^(term_display c)^","^(cast_kind_display k)^","^(term_display t)^")"
   | Prod (na,t,c) ->
       "Prod("^(name_display na)^","^(term_display t)^","^(term_display c)^")\n"
@@ -158,9 +173,9 @@ let constr_display csr =
   | Evar (e,l) -> "Evar("^(string_of_int e)^","^(array_display l)^")"
   | Const c -> "Const("^(string_of_con c)^")"
   | Ind (sp,i) ->
-      "MutInd("^(string_of_kn sp)^","^(string_of_int i)^")"
+      "MutInd("^(string_of_mind sp)^","^(string_of_int i)^")"
   | Construct ((sp,i),j) ->
-      "MutConstruct(("^(string_of_kn sp)^","^(string_of_int i)^"),"
+      "MutConstruct(("^(string_of_mind sp)^","^(string_of_int i)^"),"
       ^(string_of_int j)^")"
   | Case (ci,p,c,bl) ->
       "MutCase(<abs>,"^(term_display p)^","^(term_display c)^","
@@ -212,25 +227,25 @@ let print_pure_constr csr =
       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 ":"; box_display t; 
-      print_string ")"; print_cut(); 
+      print_string"("; print_string (string_of_id id);
+      print_string ":"; box_display t;
+      print_string ")"; print_cut();
       box_display c; close_box()
   | Prod (Anonymous,t,c) ->
       print_string"("; box_display t; print_cut(); print_string "->";
-      box_display c; print_string ")"; 
+      box_display c; print_string ")";
   | Lambda (na,t,c) ->
       print_string "["; name_display na;
       print_string ":"; box_display t; print_string "]";
-      print_cut(); box_display c; 
+      print_cut(); box_display c;
   | LetIn (na,b,t,c) ->
-      print_string "["; name_display na; print_string "="; 
+      print_string "["; name_display na; print_string "=";
       box_display b; print_cut();
       print_string ":"; box_display t; print_string "]";
-      print_cut(); box_display c; 
-  | App (c,l) -> 
-      print_string "("; 
-      box_display c; 
+      print_cut(); box_display c;
+  | App (c,l) ->
+      print_string "(";
+      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 "{";
@@ -257,25 +272,25 @@ let print_pure_constr csr =
       open_vbox 0;
       Array.iter (fun x ->  print_cut();  box_display x) bl;
       close_box();
-      print_cut(); 
-      print_string "end"; 
+      print_cut();
+      print_string "end";
       close_box()
   | Fix ((t,i),(lna,tl,bl)) ->
-      print_string "Fix("; print_int i; print_string ")"; 
+      print_string "Fix("; print_int i; print_string ")";
       print_cut();
       open_vbox 0;
       let rec print_fix () =
         for k = 0 to (Array.length tl) - 1 do
 	  open_vbox 0;
-	  name_display lna.(k); print_string "/"; 
+	  name_display lna.(k); print_string "/";
 	  print_int t.(k); print_cut(); print_string ":";
 	  box_display tl.(k) ; print_cut(); print_string ":=";
 	  box_display bl.(k); close_box ();
 	  print_cut()
         done
-      in print_string"{"; print_fix(); print_string"}" 
+      in print_string"{"; print_fix(); print_string"}"
   | CoFix(i,(lna,tl,bl)) ->
-      print_string "CoFix("; print_int i; print_string ")"; 
+      print_string "CoFix("; print_int i; print_string ")";
       print_cut();
       open_vbox 0;
       let rec print_fix () =
@@ -300,27 +315,27 @@ let print_pure_constr csr =
     | Name id -> print_string (string_of_id id)
     | Anonymous -> print_string "_"
 (* Remove the top names for library and Scratch to avoid long names *)
-  and sp_display sp = 
+  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 
+    let ls =
+      match List.rev (List.map string_of_id (repr_dirpath dir)) with
           ("Top"::l)-> l
-	| ("Coq"::_::l) -> l 
+	| ("Coq"::_::l) -> l
 	| l             -> l
     in  List.iter (fun x -> print_string x; print_string ".") ls;*)
-      print_string (string_of_kn sp)
-  and sp_con_display sp = 
+      print_string (debug_string_of_mind sp)
+  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 
+    let ls =
+      match List.rev (List.map string_of_id (repr_dirpath dir)) with
           ("Top"::l)-> l
-	| ("Coq"::_::l) -> l 
+	| ("Coq"::_::l) -> l
 	| l             -> l
     in  List.iter (fun x -> print_string x; print_string ".") ls;*)
-      print_string (string_of_con sp)
+      print_string (debug_string_of_con sp)
 
   in
-    try 
+    try
      box_display csr; print_flush()
     with e ->
 	print_string (Printexc.to_string e);print_flush ();
@@ -369,7 +384,7 @@ let pp_generic_argument arg =
 (* Vernac-level debugging commands                                    *)
 
 let in_current_context f c =
-  let (evmap,sign) = 
+  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)
@@ -400,12 +415,10 @@ let _ =
     e -> Pp.pp (Cerrors.explain_exn e)
 let _ =
   extend_vernac_command_grammar "PrintConstr"
-    [[TacTerm "PrintConstr";
-      TacNonTerm
-        (dummy_loc,
-         (Gramext.Snterm (Pcoq.Gram.Entry.obj Constr.constr),
-          ConstrArgType),
-         Some "c")]]
+    [[GramTerminal "PrintConstr";
+      GramNonTerminal
+        (dummy_loc,ConstrArgType,Extend.Aentry ("constr","constr"),
+	 Some (Names.id_of_string "c"))]]
 
 let _ =
   try
@@ -419,12 +432,10 @@ let _ =
     e -> Pp.pp (Cerrors.explain_exn e)
 let _ =
   extend_vernac_command_grammar "PrintPureConstr"
-    [[TacTerm "PrintPureConstr";
-      TacNonTerm
-        (dummy_loc,
-         (Gramext.Snterm (Pcoq.Gram.Entry.obj Constr.constr),
-          ConstrArgType),
-         Some "c")]]
+    [[GramTerminal "PrintPureConstr";
+      GramNonTerminal
+        (dummy_loc,ConstrArgType,Extend.Aentry ("constr","constr"),
+	 Some (Names.id_of_string "c"))]]
 
 (* Setting printer of unbound global reference *)
 open Names
@@ -434,38 +445,38 @@ open Libnames
 let encode_path loc prefix mpdir suffix id =
   let dir = match mpdir with
     | None -> []
-    | Some (mp,dir) -> 
+    | Some (mp,dir) ->
 	(repr_dirpath (dirpath_of_string (string_of_mp mp))@
 	repr_dirpath dir) in
-  Qualid (loc, make_qualid 
+  Qualid (loc, make_qualid
     (make_dirpath (List.rev (id_of_string prefix::dir@suffix))) id)
 
 let raw_string_of_ref loc = function
-  | ConstRef cst -> 
+  | ConstRef cst ->
       let (mp,dir,id) = repr_con cst in
       encode_path loc "CST" (Some (mp,dir)) [] (id_of_label id)
   | IndRef (kn,i) ->
-      let (mp,dir,id) = repr_kn kn in
-      encode_path loc "IND" (Some (mp,dir)) [id_of_label id] 
+      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))
-  | ConstructRef ((kn,i),j) -> 
-      let (mp,dir,id) = repr_kn kn in
+  | 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_label id;id_of_string ("_"^string_of_int i)]
 	(id_of_string ("_"^string_of_int j))
-  | VarRef id -> 
+  | 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_kn kn)))
+  | IndRef (kn,0) -> Ident (loc,id_of_label (pi3 (repr_mind kn)))
   | IndRef (kn,i) ->
-      encode_path loc "IND" None [id_of_label (pi3 (repr_kn kn))]
+      encode_path loc "IND" None [id_of_label (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_kn 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))
 
 let _ = Constrextern.set_debug_global_reference_printer
diff --git a/dev/v8-syntax/syntax-v8.tex b/dev/v8-syntax/syntax-v8.tex
index de68ce1e..46ba24da 100644
--- a/dev/v8-syntax/syntax-v8.tex
+++ b/dev/v8-syntax/syntax-v8.tex
@@ -744,28 +744,28 @@ Conflicts exists between integers and constrs.
 \nlsep \TERM{simplif}
 \nlsep \TERM{intuition}~\OPT{\NTL{tactic}{0}}
 \nlsep \TERM{linearintuition}~\OPT{\NT{num}}
-%% contrib/cc
+%% plugins/cc
 \nlsep \TERM{cc}
-%% contrib/field
+%% plugins/field
 \nlsep \TERM{field}~\STAR{\tacconstr}
-%% contrib/firstorder
+%% plugins/firstorder
 \nlsep \TERM{ground}~\OPT{\NTL{tactic}{0}}
 \nlsep \TERM{ground}~\OPT{\NTL{tactic}{0}}~\KWD{with}~\PLUS{\NT{reference}}
 \nlsep \TERM{ground}~\OPT{\NTL{tactic}{0}}~\KWD{using}~\PLUS{\NT{ident}}
 %%\nlsep \TERM{gtauto}
 \nlsep \TERM{gintuition}~\OPT{\NTL{tactic}{0}}
-%% contrib/fourier
+%% plugins/fourier
 \nlsep \TERM{fourierZ}
-%% contrib/funind
+%% plugins/funind
 \nlsep \TERM{functional}~\TERM{induction}~\tacconstr~\PLUS{\tacconstr}
-%% contrib/jprover
+%% plugins/jprover
 \nlsep \TERM{jp}~\OPT{\NT{num}}
-%% contrib/omega
+%% plugins/omega
 \nlsep \TERM{omega}
-%% contrib/ring
+%% plugins/ring
 \nlsep \TERM{quote}~\NT{ident}~\OPTGR{\KWD{[}~\PLUS{\NT{ident}}~\KWD{]}}
 \nlsep \TERM{ring}~\STAR{\tacconstr}
-%% contrib/romega
+%% plugins/romega
 \nlsep \TERM{romega}
 \SEPDEF
 \DEFNT{orient}
diff --git a/dev/vm_printers.ml b/dev/vm_printers.ml
index 1e114489..59545d8a 100644
--- a/dev/vm_printers.ml
+++ b/dev/vm_printers.ml
@@ -7,10 +7,10 @@ open Vm
 
 let ppripos (ri,pos) =
   (match ri with
-  | Reloc_annot a -> 
+  | Reloc_annot a ->
       let sp,i = a.ci.ci_ind in
-      print_string 
-	("annot : MutInd("^(string_of_kn sp)^","^(string_of_int i)^")\n")
+      print_string
+	("annot : MutInd("^(string_of_mind sp)^","^(string_of_int i)^")\n")
   | Reloc_const _ ->
       print_string "structured constant\n"
   | Reloc_getglobal kn ->
@@ -29,8 +29,8 @@ let ppsort = function
 
 
 let print_idkey idk =
-  match idk with 
-  | ConstKey sp -> 
+  match idk with
+  | ConstKey sp ->
       print_string "Cons(";
       print_string (string_of_con sp);
       print_string ")"
@@ -38,8 +38,8 @@ let print_idkey idk =
   | RelKey i -> print_string "~";print_int i
 
 let rec ppzipper z =
-  match z with 
-  | Zapp args -> 
+  match z with
+  | Zapp args ->
       let n = nargs args in
       open_hbox ();
       for i = 0 to n-2 do
@@ -50,7 +50,7 @@ let rec ppzipper z =
   | Zfix _ -> print_string "Zfix"
   | Zswitch _ -> print_string "Zswitch"
 
-and ppstack s = 
+and ppstack s =
   open_hovbox 0;
   print_string "[";
   List.iter (fun z -> ppzipper z;print_string " | ") s;
@@ -62,19 +62,19 @@ and ppatom a =
   | Aid idk -> print_idkey idk
   | Aiddef(idk,_) -> print_string "&";print_idkey idk
   | Aind(sp,i) ->  print_string "Ind(";
-      print_string (string_of_kn sp);
+      print_string (string_of_mind sp);
       print_string ","; print_int i;
       print_string ")"
 
 and ppwhd whd =
-  match whd with 
+  match whd with
   | Vsort s -> ppsort s
   | Vprod _ -> print_string "product"
   | Vfun _ -> print_string "function"
   | Vfix _ -> print_vfix()
   | Vcofix _ -> print_string "cofix"
   | Vconstr_const i -> print_string "C(";print_int i;print_string")"
-  | Vconstr_block b -> ppvblock b      
+  | Vconstr_block b -> ppvblock b
   | Vatom_stk(a,s) ->
       open_hbox();ppatom a;close_box();
       print_string"@";ppstack s