Imported Upstream version 8.4~betaupstream/8.4_beta

8 files changed, 800 insertions, 16 deletions

diff --git a/dev/doc/about-hints b/dev/doc/about-hints
new file mode 100644
index 00000000..95712c3c
--- /dev/null
+++ b/dev/doc/about-hints
@@ -0,0 +1,454 @@
+An investigation of how ZArith lemmas could be classified in different
+automation classes
+
+- Reversible lemmas relating operators (to be declared as hints but
+  needing precedences)
+- Equivalent notions (one has to be considered as primitive and the
+  other rewritten into the canonical one)
+- Isomorphisms between structure (one structure has to be considered
+  as more primitive than the other for a give operator)
+- Irreversible simplifications (to be declared with precedences)
+- Reversible bottom-up simplifications (to be used in hypotheses)
+- Irreversible bottom-up simplifications (to be used in hypotheses
+  with precedences)
+- Rewriting rules (relevant for autorewrite, or for an improved auto)
+
+Note: this analysis, made in 2001, was previously stored in
+theories/ZArith/Zhints.v. It has been moved here to avoid obfuscating
+the standard library.
+
+(**********************************************************************)
+(** *        Reversible lemmas relating operators                     *)
+(** Probably to be declared as hints but need to define precedences   *)
+
+(** ** Conversion between comparisons/predicates and arithmetic operators *)
+
+(** Lemmas ending by eq *)
+(**
+<<
+Zegal_left: (x,y:Z)`x = y`->`x+(-y) = 0`
+Zabs_eq: (x:Z)`0 <= x`->`|x| = x`
+Zeven_div2: (x:Z)(Zeven x)->`x = 2*(Zdiv2 x)`
+Zodd_div2: (x:Z)`x >= 0`->(Zodd x)->`x = 2*(Zdiv2 x)+1`
+>>
+*)
+
+(** Lemmas ending by Zgt *)
+(**
+<<
+Zgt_left_rev: (x,y:Z)`x+(-y) > 0`->`x > y`
+Zgt_left_gt: (x,y:Z)`x > y`->`x+(-y) > 0`
+>>
+*)
+
+(** Lemmas ending by Zlt *)
+(**
+<<
+Zlt_left_rev: (x,y:Z)`0 < y+(-x)`->`x < y`
+Zlt_left_lt: (x,y:Z)`x < y`->`0 < y+(-x)`
+Zlt_O_minus_lt: (n,m:Z)`0 < n-m`->`m < n`
+>>
+*)
+
+(** Lemmas ending by Zle *)
+(**
+<<
+Zle_left: (x,y:Z)`x <= y`->`0 <= y+(-x)`
+Zle_left_rev: (x,y:Z)`0 <= y+(-x)`->`x <= y`
+Zlt_left: (x,y:Z)`x < y`->`0 <= y+(-1)+(-x)`
+Zge_left: (x,y:Z)`x >= y`->`0 <= x+(-y)`
+Zgt_left: (x,y:Z)`x > y`->`0 <= x+(-1)+(-y)`
+>>
+*)
+
+(** ** Conversion between nat comparisons and Z comparisons *)
+
+(** Lemmas ending by eq *)
+(**
+<<
+inj_eq: (x,y:nat)x=y->`(inject_nat x) = (inject_nat y)`
+>>
+*)
+
+(** Lemmas ending by Zge *)
+(**
+<<
+inj_ge: (x,y:nat)(ge x y)->`(inject_nat x) >= (inject_nat y)`
+>>
+*)
+
+(** Lemmas ending by Zgt *)
+(**
+<<
+inj_gt: (x,y:nat)(gt x y)->`(inject_nat x) > (inject_nat y)`
+>>
+*)
+
+(** Lemmas ending by Zlt *)
+(**
+<<
+inj_lt: (x,y:nat)(lt x y)->`(inject_nat x) < (inject_nat y)`
+>>
+*)
+
+(** Lemmas ending by Zle *)
+(**
+<<
+inj_le: (x,y:nat)(le x y)->`(inject_nat x) <= (inject_nat y)`
+>>
+*)
+
+(** ** Conversion between comparisons *)
+
+(** Lemmas ending by Zge *)
+(**
+<<
+not_Zlt: (x,y:Z)~`x < y`->`x >= y`
+Zle_ge: (m,n:Z)`m <= n`->`n >= m`
+>>
+*)
+
+(** Lemmas ending by Zgt *)
+(**
+<<
+Zle_gt_S: (n,p:Z)`n <= p`->`(Zs p) > n`
+not_Zle: (x,y:Z)~`x <= y`->`x > y`
+Zlt_gt: (m,n:Z)`m < n`->`n > m`
+Zle_S_gt: (n,m:Z)`(Zs n) <= m`->`m > n`
+>>
+*)
+
+(** Lemmas ending by Zlt *)
+(**
+<<
+not_Zge: (x,y:Z)~`x >= y`->`x < y`
+Zgt_lt: (m,n:Z)`m > n`->`n < m`
+Zle_lt_n_Sm: (n,m:Z)`n <= m`->`n < (Zs m)`
+>>
+*)
+
+(** Lemmas ending by Zle *)
+(**
+<<
+Zlt_ZERO_pred_le_ZERO: (x:Z)`0 < x`->`0 <= (Zpred x)`
+not_Zgt: (x,y:Z)~`x > y`->`x <= y`
+Zgt_le_S: (n,p:Z)`p > n`->`(Zs n) <= p`
+Zgt_S_le: (n,p:Z)`(Zs p) > n`->`n <= p`
+Zge_le: (m,n:Z)`m >= n`->`n <= m`
+Zlt_le_S: (n,p:Z)`n < p`->`(Zs n) <= p`
+Zlt_n_Sm_le: (n,m:Z)`n < (Zs m)`->`n <= m`
+Zlt_le_weak: (n,m:Z)`n < m`->`n <= m`
+Zle_refl: (n,m:Z)`n = m`->`n <= m`
+>>
+*)
+
+(** ** Irreversible simplification involving several comparaisons *)
+(**    useful with clear precedences *)
+
+(** Lemmas ending by Zlt *)
+(**
+<<
+Zlt_le_reg :(a,b,c,d:Z)`a < b`->`c <= d`->`a+c < b+d`
+Zle_lt_reg : (a,b,c,d:Z)`a <= b`->`c < d`->`a+c < b+d`
+>>
+*)
+
+(** ** What is decreasing here ? *)
+
+(** Lemmas ending by eq *)
+(**
+<<
+Zplus_minus: (n,m,p:Z)`n = m+p`->`p = n-m`
+>>
+*)
+
+(** Lemmas ending by Zgt *)
+(**
+<<
+Zgt_pred: (n,p:Z)`p > (Zs n)`->`(Zpred p) > n`
+>>
+*)
+
+(** Lemmas ending by Zlt *)
+(**
+<<
+Zlt_pred: (n,p:Z)`(Zs n) < p`->`n < (Zpred p)`
+>>
+*)
+
+(**********************************************************************)
+(** *                Useful Bottom-up lemmas                          *)
+
+(** ** Bottom-up simplification: should be used *)
+
+(** Lemmas ending by eq *)
+(**
+<<
+Zeq_add_S: (n,m:Z)`(Zs n) = (Zs m)`->`n = m`
+Zsimpl_plus_l: (n,m,p:Z)`n+m = n+p`->`m = p`
+Zplus_unit_left: (n,m:Z)`n+0 = m`->`n = m`
+Zplus_unit_right: (n,m:Z)`n = m+0`->`n = m`
+>>
+*)
+
+(** Lemmas ending by Zgt *)
+(**
+<<
+Zsimpl_gt_plus_l: (n,m,p:Z)`p+n > p+m`->`n > m`
+Zsimpl_gt_plus_r: (n,m,p:Z)`n+p > m+p`->`n > m`
+Zgt_S_n: (n,p:Z)`(Zs p) > (Zs n)`->`p > n`
+>>
+*)
+
+(** Lemmas ending by Zlt *)
+(**
+<<
+Zsimpl_lt_plus_l: (n,m,p:Z)`p+n < p+m`->`n < m`
+Zsimpl_lt_plus_r: (n,m,p:Z)`n+p < m+p`->`n < m`
+Zlt_S_n: (n,m:Z)`(Zs n) < (Zs m)`->`n < m`
+>>
+*)
+
+(** Lemmas ending by Zle *)
+(** << Zsimpl_le_plus_l: (p,n,m:Z)`p+n <= p+m`->`n <= m`
+Zsimpl_le_plus_r: (p,n,m:Z)`n+p <= m+p`->`n <= m`
+Zle_S_n: (n,m:Z)`(Zs m) <= (Zs n)`->`m <= n` >> *)
+
+(** ** Bottom-up irreversible (syntactic) simplification *)
+
+(** Lemmas ending by Zle *)
+(**
+<<
+Zle_trans_S: (n,m:Z)`(Zs n) <= m`->`n <= m`
+>>
+*)
+
+(** ** Other unclearly simplifying lemmas *)
+
+(** Lemmas ending by Zeq *)
+(**
+<<
+Zmult_eq: (x,y:Z)`x <> 0`->`y*x = 0`->`y = 0`
+>>
+*)
+
+(* Lemmas ending by Zgt *)
+(**
+<<
+Zmult_gt: (x,y:Z)`x > 0`->`x*y > 0`->`y > 0`
+>>
+*)
+
+(* Lemmas ending by Zlt *)
+(**
+<<
+pZmult_lt: (x,y:Z)`x > 0`->`0 < y*x`->`0 < y`
+>>
+*)
+
+(* Lemmas ending by Zle *)
+(**
+<<
+Zmult_le: (x,y:Z)`x > 0`->`0 <= y*x`->`0 <= y`
+OMEGA1: (x,y:Z)`x = y`->`0 <= x`->`0 <= y`
+>>
+*)
+
+
+(**********************************************************************)
+(** *        Irreversible lemmas with meta-variables                  *)
+(** To be used by EAuto                                               *)
+
+(* Hints Immediate *)
+(** Lemmas ending by eq *)
+(**
+<<
+Zle_antisym: (n,m:Z)`n <= m`->`m <= n`->`n = m`
+>>
+*)
+
+(** Lemmas ending by Zge *)
+(**
+<<
+Zge_trans: (n,m,p:Z)`n >= m`->`m >= p`->`n >= p`
+>>
+*)
+
+(** Lemmas ending by Zgt *)
+(**
+<<
+Zgt_trans: (n,m,p:Z)`n > m`->`m > p`->`n > p`
+Zgt_trans_S: (n,m,p:Z)`(Zs n) > m`->`m > p`->`n > p`
+Zle_gt_trans: (n,m,p:Z)`m <= n`->`m > p`->`n > p`
+Zgt_le_trans: (n,m,p:Z)`n > m`->`p <= m`->`n > p`
+>>
+*)
+
+(** Lemmas ending by Zlt *)
+(**
+<<
+Zlt_trans: (n,m,p:Z)`n < m`->`m < p`->`n < p`
+Zlt_le_trans: (n,m,p:Z)`n < m`->`m <= p`->`n < p`
+Zle_lt_trans: (n,m,p:Z)`n <= m`->`m < p`->`n < p`
+>>
+*)
+
+(** Lemmas ending by Zle *)
+(**
+<<
+Zle_trans: (n,m,p:Z)`n <= m`->`m <= p`->`n <= p`
+>>
+*)
+
+
+(**********************************************************************)
+(** *               Unclear or too specific lemmas                    *)
+(** Not to be used ?                                                  *)
+
+(** ** Irreversible and too specific (not enough regular) *)
+
+(** Lemmas ending by Zle *)
+(**
+<<
+Zle_mult: (x,y:Z)`x > 0`->`0 <= y`->`0 <= y*x`
+Zle_mult_approx: (x,y,z:Z)`x > 0`->`z > 0`->`0 <= y`->`0 <= y*x+z`
+OMEGA6: (x,y,z:Z)`0 <= x`->`y = 0`->`0 <= x+y*z`
+OMEGA7: (x,y,z,t:Z)`z > 0`->`t > 0`->`0 <= x`->`0 <= y`->`0 <= x*z+y*t`
+>>
+*)
+
+(** ** Expansion and too specific ? *)
+
+(** Lemmas ending by Zge *)
+(**
+<<
+Zge_mult_simpl: (a,b,c:Z)`c > 0`->`a*c >= b*c`->`a >= b`
+>>
+*)
+
+(** Lemmas ending by Zgt *)
+(**
+<<
+Zgt_mult_simpl: (a,b,c:Z)`c > 0`->`a*c > b*c`->`a > b`
+Zgt_square_simpl: (x,y:Z)`x >= 0`->`y >= 0`->`x*x > y*y`->`x > y`
+>>
+*)
+
+(** Lemmas ending by Zle *)
+(**
+<<
+Zle_mult_simpl: (a,b,c:Z)`c > 0`->`a*c <= b*c`->`a <= b`
+Zmult_le_approx: (x,y,z:Z)`x > 0`->`x > z`->`0 <= y*x+z`->`0 <= y`
+>>
+*)
+
+(** ** Reversible but too specific ? *)
+
+(** Lemmas ending by Zlt *)
+(**
+<<
+Zlt_minus: (n,m:Z)`0 < m`->`n-m < n`
+>>
+*)
+
+(**********************************************************************)
+(** *               Lemmas to be used as rewrite rules                *)
+(** but can also be used as hints                                     *)
+
+(** Left-to-right simplification lemmas (a symbol disappears) *)
+
+(**
+<<
+Zcompare_n_S: (n,m:Z)(Zcompare (Zs n) (Zs m))=(Zcompare n m)
+Zmin_n_n: (n:Z)`(Zmin n n) = n`
+Zmult_1_n: (n:Z)`1*n = n`
+Zmult_n_1: (n:Z)`n*1 = n`
+Zminus_plus: (n,m:Z)`n+m-n = m`
+Zle_plus_minus: (n,m:Z)`n+(m-n) = m`
+Zopp_Zopp: (x:Z)`(-(-x)) = x`
+Zero_left: (x:Z)`0+x = x`
+Zero_right: (x:Z)`x+0 = x`
+Zplus_inverse_r: (x:Z)`x+(-x) = 0`
+Zplus_inverse_l: (x:Z)`(-x)+x = 0`
+Zopp_intro: (x,y:Z)`(-x) = (-y)`->`x = y`
+Zmult_one: (x:Z)`1*x = x`
+Zero_mult_left: (x:Z)`0*x = 0`
+Zero_mult_right: (x:Z)`x*0 = 0`
+Zmult_Zopp_Zopp: (x,y:Z)`(-x)*(-y) = x*y`
+>>
+*)
+
+(** Right-to-left simplification lemmas (a symbol disappears) *)
+
+(**
+<<
+Zpred_Sn: (m:Z)`m = (Zpred (Zs m))`
+Zs_pred: (n:Z)`n = (Zs (Zpred n))`
+Zplus_n_O: (n:Z)`n = n+0`
+Zmult_n_O: (n:Z)`0 = n*0`
+Zminus_n_O: (n:Z)`n = n-0`
+Zminus_n_n: (n:Z)`0 = n-n`
+Zred_factor6: (x:Z)`x = x+0`
+Zred_factor0: (x:Z)`x = x*1`
+>>
+*)
+
+(** Unclear orientation (no symbol disappears) *)
+
+(**
+<<
+Zplus_n_Sm: (n,m:Z)`(Zs (n+m)) = n+(Zs m)`
+Zmult_n_Sm: (n,m:Z)`n*m+n = n*(Zs m)`
+Zmin_SS: (n,m:Z)`(Zs (Zmin n m)) = (Zmin (Zs n) (Zs m))`
+Zplus_assoc_l: (n,m,p:Z)`n+(m+p) = n+m+p`
+Zplus_assoc_r: (n,m,p:Z)`n+m+p = n+(m+p)`
+Zplus_permute: (n,m,p:Z)`n+(m+p) = m+(n+p)`
+Zplus_Snm_nSm: (n,m:Z)`(Zs n)+m = n+(Zs m)`
+Zminus_plus_simpl: (n,m,p:Z)`n-m = p+n-(p+m)`
+Zminus_Sn_m: (n,m:Z)`(Zs (n-m)) = (Zs n)-m`
+Zmult_plus_distr_l: (n,m,p:Z)`(n+m)*p = n*p+m*p`
+Zmult_minus_distr: (n,m,p:Z)`(n-m)*p = n*p-m*p`
+Zmult_assoc_r: (n,m,p:Z)`n*m*p = n*(m*p)`
+Zmult_assoc_l: (n,m,p:Z)`n*(m*p) = n*m*p`
+Zmult_permute: (n,m,p:Z)`n*(m*p) = m*(n*p)`
+Zmult_Sm_n: (n,m:Z)`n*m+m = (Zs n)*m`
+Zmult_Zplus_distr: (x,y,z:Z)`x*(y+z) = x*y+x*z`
+Zmult_plus_distr: (n,m,p:Z)`(n+m)*p = n*p+m*p`
+Zopp_Zplus: (x,y:Z)`(-(x+y)) = (-x)+(-y)`
+Zplus_sym: (x,y:Z)`x+y = y+x`
+Zplus_assoc: (x,y,z:Z)`x+(y+z) = x+y+z`
+Zmult_sym: (x,y:Z)`x*y = y*x`
+Zmult_assoc: (x,y,z:Z)`x*(y*z) = x*y*z`
+Zopp_Zmult: (x,y:Z)`(-x)*y = (-(x*y))`
+Zplus_S_n: (x,y:Z)`(Zs x)+y = (Zs (x+y))`
+Zopp_one: (x:Z)`(-x) = x*(-1)`
+Zopp_Zmult_r: (x,y:Z)`(-(x*y)) = x*(-y)`
+Zmult_Zopp_left: (x,y:Z)`(-x)*y = x*(-y)`
+Zopp_Zmult_l: (x,y:Z)`(-(x*y)) = (-x)*y`
+Zred_factor1: (x:Z)`x+x = x*2`
+Zred_factor2: (x,y:Z)`x+x*y = x*(1+y)`
+Zred_factor3: (x,y:Z)`x*y+x = x*(1+y)`
+Zred_factor4: (x,y,z:Z)`x*y+x*z = x*(y+z)`
+Zminus_Zplus_compatible: (x,y,n:Z)`x+n-(y+n) = x-y`
+Zmin_plus: (x,y,n:Z)`(Zmin (x+n) (y+n)) = (Zmin x y)+n`
+>>
+*)
+
+(** nat <-> Z *)
+(**
+<<
+inj_S: (y:nat)`(inject_nat (S y)) = (Zs (inject_nat y))`
+inj_plus: (x,y:nat)`(inject_nat (plus x y)) = (inject_nat x)+(inject_nat y)`
+inj_mult: (x,y:nat)`(inject_nat (mult x y)) = (inject_nat x)*(inject_nat y)`
+inj_minus1:
+ (x,y:nat)(le y x)->`(inject_nat (minus x y)) = (inject_nat x)-(inject_nat y)`
+inj_minus2: (x,y:nat)(gt y x)->`(inject_nat (minus x y)) = 0`
+>>
+*)
+
+(** Too specific ? *)
+(**
+<<
+Zred_factor5: (x,y:Z)`x*0+y = y`
+>>
+*)
diff --git a/dev/doc/build-system.dev.txt b/dev/doc/build-system.dev.txt
index d4014303..3d9cba14 100644
--- a/dev/doc/build-system.dev.txt
+++ b/dev/doc/build-system.dev.txt
@@ -1,6 +1,22 @@
+
 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 internals of the implementation of the build
 system. For what a Coq developer needs to know about the build system,
 see build-system.txt .
diff --git a/dev/doc/build-system.txt b/dev/doc/build-system.txt
index 9362aeeb..b243ebe2 100644
--- a/dev/doc/build-system.txt
+++ b/dev/doc/build-system.txt
@@ -1,12 +1,60 @@
 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.
 
+
+FAQ: special features used in this Makefile
+-------------------------------------------
+
+* Order-only dependencies: |
+
+Dependencies placed after a bar (|) should be built before
+the current rule, but having one of them is out-of-date do not
+trigger a rebuild of the current rule.
+See http://www.gnu.org/software/make/manual/make.htmlPrerequisite-Types
+
+* Annotation before commands: +/-/@
+
+a command starting by - is always successful (errors are ignored)
+a command starting by + is runned even if option -n is given to make
+a command starting by @ is not echoed before being runned
+
+* Custom functions
+
+Definition via "define foo" followed by commands (arg is $(1) etc)
+Call via "$(call foo,arg1)"
+
+* Useful builtin functions
+
+$(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
 ----------------------
 
diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index 069f7d42..322530e6 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -1,4 +1,43 @@
 =========================================
+= CHANGES BETWEEN COQ V8.3 AND COQ V8.4 =
+=========================================
+
+** Functions in unification.ml have now the evar_map coming just after the env
+
+** Removal of Tacinterp.constr_of_id **
+
+Use instead either global_reference or construct_reference in constrintern.ml.
+
+** Optimizing calls to Evd functions **
+
+Evars are split into defined evars and undefined evars; for
+efficiency, when an evar is known to be undefined, it is preferable to
+use specific functions about undefined evars since these ones are
+generally fewer than the defined ones.
+
+** Type changes in TACTIC EXTEND rules **
+
+Arguments bound with tactic(_) in TACTIC EXTEND rules are now of type
+glob_tactic_expr, instead of glob_tactic_expr * tactic. Only the first
+component is kept, the second one can be obtained via
+Tacinterp.eval_tactic.
+
+** ARGUMENT EXTEND **
+
+It is now forbidden to use TYPED simultaneously with {RAW,GLOB}_TYPED
+in ARGUMENT EXTEND statements.
+
+** Renaming of rawconstr to glob_constr **
+
+The "rawconstr" type has been renamed to "glob_constr" for
+consistency. The "raw" in everything related to former rawconstr has
+been changed to "glob". For more details about the rationale and
+scripts to migrate code using Coq's internals, see commits 13743,
+13744, 13755, 13756, 13757, 13758, 13761 (by glondu, end of December
+2010) in Subversion repository. Contribs have been fixed too, and
+commit messages there might also be helpful for migrating.
+
+=========================================
 = CHANGES BETWEEN COQ V8.2 AND COQ V8.3 =
 =========================================
 
diff --git a/dev/doc/debugging.txt b/dev/doc/debugging.txt
index 50b3b45c..2480b8ed 100644
--- a/dev/doc/debugging.txt
+++ b/dev/doc/debugging.txt
@@ -11,6 +11,12 @@ Debugging from Coq toplevel using Caml trace mechanism
   6. Test your Coq command and observe the result of tracing your functions
   7. Freely switch from Coq to Ocaml toplevels with 'Drop.' and 'go();;'
 
+  You can avoid typing #use "include" (or "base_include") after Drop
+  by adding the following lines in your $HOME/.ocamlinit :
+
+   if Filename.basename Sys.argv.(0) = "coqtop.byte"
+   then ignore (Toploop.use_silently Format.std_formatter "include")
+
   Hints: To remove high-level pretty-printing features (coercions,
   notations, ...), use "Set Printing All". It will affect the #trace
   printers too.
diff --git a/dev/doc/perf-analysis b/dev/doc/perf-analysis
index d23bf835..ac54fa6f 100644
--- a/dev/doc/perf-analysis
+++ b/dev/doc/perf-analysis
@@ -1,13 +1,32 @@
 Performance analysis (trunk repository)
 ---------------------------------------
 
+Jun 7, 2010: delayed re-typing of Ltac instances in matching
+  (-1% on HighSchoolGeometry, -2% on JordanCurveTheorem)
+
+Jun 4, 2010: improvement in eauto and type classes inference by removing
+  systematic preparation of debugging pretty-printing streams (std_ppcmds)
+  (-7% in ATBR, visible only on V8.3 logs since ATBR is broken in trunk;
+   -6% in HighSchoolGeometry)
+
+Apr 19, 2010: small improvement obtained by reducing evar instantiation 
+  from O(n^3) to O(n^2) in the size of the instance (-2% in Compcert,
+  -2% AreaMethod, -15% in Ssreflect)
+
+Apr 17, 2010: small improvement obtained by not repeating unification
+  twice in auto (-2% in Compcert, -2% in Algebra)
+
+Feb 15, 2010: Global decrease due to unicode inefficiency repaired
+
+Jan 8, 2010: Global increase due to an inefficiency in unicode treatment
+
 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 
+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/unification.txt b/dev/doc/unification.txt
new file mode 100644
index 00000000..6d05bcf5
--- /dev/null
+++ b/dev/doc/unification.txt
@@ -0,0 +1,208 @@
+Some notes about the use of unification in Coq
+----------------------------------------------
+
+There are several applications of unification and pattern-matching
+
+** Unification of types **
+
+- For type inference, inference of implicit arguments
+  * this basically amounts to solve problems of the form T <= U or T = U
+    where T and U are types coming from a given typing problem
+  * this kind of problem has to succeed and all the power of unification is
+    a priori expected (full beta/delta/iota/zeta/nu/mu, pattern-unification,
+    pruning, imitation/projection heuristics, ...)
+
+- For lemma application (apply, auto, ...)
+  * these are also problems of the form T <= U on types but with T
+    coming from a lemma and U from the goal
+  * it is not obvious that we always want unification and not matching
+  * it is not clear which amounts of delta one wants to use
+
+** Looking for subterms **
+
+- For tactics applying on subterms: induction, destruct, rewrite
+
+- As part of unification of types in the presence of higher-order
+  evars (e.g. when applying a lemma of conclusion "?P t")
+
+
+----------------------------------------------------------------------
+Here are examples of features one may want or not when looking for subterms
+
+A- REWRITING
+
+1- Full conversion on closed terms
+
+1a- Full conversion on closed terms in the presence of at least one evars (meta)
+
+Section A1.
+Variable y: nat.
+Hypothesis H: forall x, x+2 = 0.
+Goal y+(1+1) = 0.
+rewrite H.
+(* 0 = 0 *)
+Abort.
+
+Goal 2+(1+1) = 0.
+rewrite H.
+(* 0 = 0 *)
+Abort.
+
+(* This exists since the very beginning of Chet's unification for tactics *)
+(* But this fails for setoid rewrite *)
+
+1b- Full conversion on closed terms without any evars in the lemma
+
+1b.1- Fails on rewrite (because Unification.w_unify_to_subterm_list replaces
+  unification by check for a syntactic subterm if terms has no evar/meta)
+
+Goal 0+1 = 0 -> 0+(1+0) = 0.
+intros H; rewrite H.
+(* fails *)
+Abort.
+
+1b.2- Works with setoid rewrite
+
+Require Import Setoid.
+Goal 0+1 = 0 -> 0+(1+0) = 0.
+intros H; rewrite H at 1.
+(* 0 = 0 *)
+Abort.
+
+2- Using known instances in full conversion on closed terms
+
+Section A2.
+Hypothesis H: forall x, x+(2+x) = 0.
+Goal 1+(1+2) = 0.
+rewrite H.
+Abort.
+End A2.
+
+(* This exists since 8.2 (HH) *)
+
+3- Pattern-unification on Rels
+
+Section A3a.
+Variable F: (nat->nat->nat)->nat.
+Goal exists f, F (fun x y => f x y) = 0 -> F (fun x y => plus y x) = 0.
+eexists. intro H; rewrite H.
+(* 0 = 0 *)
+Abort.
+End A3a.
+
+(* Works since pattern unification on Meta applied to Rel was introduced *)
+(* in unification.ml (8.1, Sep 2006, HH) *)
+
+Section A3b.
+Variables x y: nat.
+Variable H: forall f, f x y = 0.
+Goal plus y x = 0.
+rewrite H.
+(* 0 = 0 *)
+Abort.
+End A3b.
+
+(* Works since pattern unification on all Meta was supported *)
+(* in unification.ml (8.4, Jun 2011, HH) *)
+
+4- Unification with open terms
+
+Section A4.
+Hypothesis H: forall x, S x = 0.
+Goal S 0 = 0.
+rewrite (H _).
+(* 0 = 0 *)
+Abort.
+End A4.
+
+(* Works since unification on Evar was introduced so as to support rewriting *)
+(* with open terms (8.2, MS, r11543, Unification.w_unify_to_subterm_list ) *)
+
+5- Unification of pre-existing evars
+
+5a- Basic unification of pre-existing evars
+
+Section A4.
+Variables x y: nat.
+Goal exists z, S z = 0 -> S (plus y x) = 0.
+eexists. intro H; rewrite H.
+(* 0 = 0 *)
+Abort.
+End A4.
+
+(* This worked in 8.2 and 8.3 as a side-effect of support for rewriting *)
+(* with open terms (8.2, MS, r11543) *)
+
+5b- Pattern-unification of pre-existing evars in rewriting lemma
+
+Goal exists f, forall x y, f x y = 0 -> plus y x = 0.
+eexists. intros x y H; rewrite H.
+(* 0 = 0 *)
+Abort.
+
+(* Works since pattern-unification on Evar was introduced *)
+(* in unification.ml (8.3, HH, r12229) *)
+(* currently governed by a flag: use_evars_pattern_unification *)
+
+5c- Pattern-unification of pre-existing evars in goal
+
+Goal exists f, forall x y, plus x y = 0 -> f y x = 0.
+eexists. intros x y H; rewrite H.
+(* 0 = 0 *)
+Abort.
+
+(* This worked in 8.2 and 8.3 but was removed for autorewrite in 8.4 *)
+
+5d- Mixing pattern-unification of pre-existing evars in goal and evars in lemma
+
+Goal exists f, forall x, (forall y, plus x y = 0) -> forall y:nat, f y x = 0.
+eexists. intros x H y. rewrite H.
+(* 0 = 0 *)
+Abort.
+
+(* This worked in 8.2 and 8.3 but was removed for autorewrite in 8.4 *)
+
+6- Multiple non-identical but convertible occurrences
+
+Tactic rewrite only considers the first one, from left-to-right, e.g.:
+
+Section A6.
+Variable y: nat.
+Hypothesis H: forall x, x+2 = 0.
+Goal (y+(2+0))+(y+(1+1)) = (y+(1+1))+(y+(2+0)).
+rewrite H.
+(* 0+(y+(1+1)) = y+(1+1)+0 *)
+Abort.
+End A6.
+
+Tactic setoid rewrite first looks for syntactically equal terms and if
+not uses the leftmost occurrence modulo delta.
+
+Require Import Setoid.
+Section A6.
+Variable y: nat.
+Hypothesis H: forall x, x+2 = 0.
+Goal (y+(2+0))+(y+2) = (y+2)+(y+(2+0)).
+rewrite H at 1 2 3 4.
+(* (y+(2+0))+0 = 0+(y+(2+0)) *)
+Abort.
+
+Goal (y+(2+0))+(y+(1+1)) = (y+(1+1))+(y+(2+0)).
+rewrite H at 1 2 3 4.
+(* 0+(y+(1+1)) = y+(1+1)+0 *)
+Abort.
+End A6.
+
+7- Conversion
+
+Section A6.
+Variable y: nat.
+Hypothesis H: forall x, S x = 0.
+Goal id 1 = 0.
+rewrite H.
+
+
+B- ELIMINATION (INDUCTION / CASE ANALYSIS)
+
+This is simpler because open terms are not allowed and no unification
+is involved (8.3).
diff --git a/dev/doc/universes.txt b/dev/doc/universes.txt
index 65c1e522..a40706e9 100644
--- a/dev/doc/universes.txt
+++ b/dev/doc/universes.txt
@@ -1,32 +1,26 @@
 How to debug universes?
 
-1. There is a command Dump Universes in Coq toplevel
+1. There is a command Print Universes in Coq toplevel
 
-   Dump Universes.
+   Print Universes.
      prints the graph of universes in the form of constraints
 
-   Dump Universes "file".
+   Print Universes "file".
      produces the "file" containing universe constraints in the form
        univ1 # univ2 ;
      where # can be either > >= or =
-     
-   The file produced by the latter command can be transformed using
-   the script univdot to dot format.
-   For example
 
-   univdot file | dot -Tps > file.ps
-
-   produces a graph of universes in ps format. 
-   > arrows are red, >= blue, and = black.
+   If "file" ends with .gv or .dot, the resulting file will be in
+   dot format.
 
 
    *) for dot see http://www.research.att.com/sw/tools/graphviz/
 
 
 2. There is a printing option
-  
-   Termast.print_universes : bool ref
 
-   which, when set (in ocaml after Drop), makes all pretty-printed
-   Type's annotated with the name of the universe.
+   {Set,Unset} Printing Universes.
+
+   which, when set, makes all pretty-printed Type's annotated with the
+   name of the universe.