Imported Upstream version 8.4~betaupstream/8.4_beta

author: Stephane Glondu <steph@glondu.net> 2012-01-12 16:02:20 +0100
committer: Stephane Glondu <steph@glondu.net> 2012-01-12 16:02:20 +0100
commit: 97fefe1fcca363a1317e066e7f4b99b9c1e9987b (patch)
tree: 97ec6b7d831cc5fb66328b0c63a11db1cbb2f158 /test-suite
parent: 300293c119981054c95182a90c829058530a6b6f (diff)
157 files changed, 4024 insertions, 434 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile
index 98bab43b..cd5886f8 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -75,7 +75,7 @@ VSUBSYSTEMS := prerequisite success failure $(BUGS) output \
   interactive micromega $(COMPLEXITY) modules
 
 # All subsystems
-SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs
+SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs ide
 
 #######################################################################
 # Phony targets
@@ -94,12 +94,9 @@ clean:
 	rm -f trace lia.cache
 	$(SHOW) "RM        <**/*.stamp> <**/*.vo> <**/*.log>"
 	$(HIDE)find . \( \
-	  -name '*.stamp' -o -name '*.vo' -o -name '*.v.log' \
+	  -name '*.stamp' -o -name '*.vo' -o -name '*.log' \
 	\) -print0 | xargs -0 rm -f
 
-distclean: clean
-	$(HIDE)find . -name '*.log' -print0 | xargs -0 rm -f
-
 #######################################################################
 # Per-subsystem targets
 #######################################################################
@@ -115,7 +112,7 @@ $(foreach S,$(VSUBSYSTEMS),$(eval $(call mkstamp,$(S))))
 # Summary
 #######################################################################
 
-summary_dir = echo $(1); find $(2) -name '*.log' -print0 | xargs -0 tail -q -n1 | sort -g
+summary_dir = echo $(1); find $(2) -name '*.log' -print0 | xargs -0 -n 1 tail -n1 | sort -g
 
 .PHONY: summary summary.log
 
@@ -131,6 +128,7 @@ summary:
 	  $(call summary_dir, "Miscellaneous tests", misc); \
 	  $(call summary_dir, "Complexity tests", complexity); \
 	  $(call summary_dir, "Module tests", modules); \
+	  $(call summary_dir, "IDE tests", ide); \
 	  nb_success=`find . -name '*.log' -exec tail -n2 '{}' \; | grep -e $(log_success) | wc -l`; \
 	  nb_failure=`find . -name '*.log' -exec tail -n2 '{}' \; | grep -e $(log_failure) | wc -l`; \
 	  nb_tests=`expr $$nb_success + $$nb_failure`; \
@@ -271,7 +269,7 @@ $(addsuffix .log,$(wildcard output/*.v)): %.v.log: %.v
 	    | grep -v "Welcome to Coq" \
 	    | grep -v "Skipping rcfile loading" \
 	    > $$tmpoutput; \
-	  diff $$tmpoutput $*.out 2>&1; R=$$?; times; \
+	  diff -u $*.out $$tmpoutput 2>&1; R=$$?; times; \
 	  if [ $$R = 0 ]; then \
 	    echo $(log_success); \
 	    echo "    $<...Ok"; \
@@ -354,7 +352,7 @@ $(addsuffix .log,$(wildcard modules/*.v)): %.v.log: modules/Nat.vo modules/plik.
 # Miscellaneous tests
 #######################################################################
 
-misc: misc/xml.log misc/deps-order.log
+misc: misc/xml.log misc/deps-order.log misc/universes.log
 
 # Test xml compilation
 xml: misc/xml.log
@@ -371,7 +369,7 @@ misc/xml.log:
 	  else \
 	    echo $(log_success); \
 	    echo "    misc/xml...apparently ok"; \
-	  fi; rm -r misc/xml; \
+	  fi; rm -rf misc/xml; \
 	} > "$@"
 
 # Check that both coqdep and coqtop/coqc takes the later -I/-R
@@ -386,7 +384,7 @@ misc/deps-order.log:
 	  tmpoutput=`mktemp /tmp/coqcheck.XXXXXX`; \
 	  $(coqdep) -I misc/deps/lib -as lib -R misc/deps/client client misc/deps/client/bar.v 2>&1 \
 	    | head -n 1 > $$tmpoutput; \
-	  diff $$tmpoutput misc/deps/deps.out 2>&1; R=$$?; times; \
+	  diff -u misc/deps/deps.out $$tmpoutput 2>&1; R=$$?; times; \
 	  $(bincoqc) -I misc/deps/lib -as lib misc/deps/lib/foo.v 2>&1; \
 	  $(bincoqc) -I misc/deps/lib -as lib -R misc/deps/client client misc/deps/client/foo.v 2>&1; \
 	  $(coqtop) -I misc/deps/lib -as lib -R misc/deps/client client -load-vernac-source misc/deps/client/bar.v 2>&1; \
@@ -400,3 +398,45 @@ misc/deps-order.log:
 	  fi; \
 	  rm $$tmpoutput; \
 	} > "$@"
+
+# Sort universes for the whole standard library
+EXPECTED_UNIVERSES := 3
+universes: misc/universes.log
+misc/universes.log: misc/universes/all_stdlib.v
+	@echo "TEST      misc/universes"
+	$(HIDE){ \
+	  $(bincoqc) -I misc/universes misc/universes/all_stdlib 2>&1; \
+	  $(bincoqc) -I misc/universes misc/universes/universes 2>&1; \
+	  mv universes.txt misc/universes; \
+	  N=`awk '{print $$3}' misc/universes/universes.txt | sort -u | wc -l`; \
+	  times; \
+	  if [ "$$N" -eq $(EXPECTED_UNIVERSES) ]; then \
+	    echo $(log_success); \
+	    echo "    misc/universes...Ok ($(EXPECTED_UNIVERSES) universes)"; \
+	  else \
+	    echo $(log_failure); \
+	    echo "    misc/universes...Error! ($$N/$(EXPECTED_UNIVERSES) universes)"; \
+	  fi; \
+	} > "$@"
+
+misc/universes/all_stdlib.v:
+	cd .. && $(MAKE) test-suite/$@
+
+
+# IDE : some tests of backtracking for coqtop -ideslave
+
+ide : $(patsubst %.fake,%.fake.log,$(wildcard ide/*.fake))
+
+%.fake.log : %.fake
+	@echo "TEST      $<"
+	$(HIDE){ \
+	  echo $(call log_intro,$<); \
+	  $(BIN)fake_ide "$(BIN)coqtop -boot" < $< 2>&1; \
+	  if [ $$? = 0 ]; then \
+	    echo $(log_success); \
+	    echo "    $<...Ok"; \
+	  else \
+	    echo $(log_failure); \
+	    echo "    $<...Error!"; \
+	  fi; \
+	} > "$@"
diff --git a/test-suite/bench/lists-100.v b/test-suite/bench/lists-100.v
index 490de2a6..3d145d96 100644
--- a/test-suite/bench/lists-100.v
+++ b/test-suite/bench/lists-100.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/test-suite/bench/lists_100.v b/test-suite/bench/lists_100.v
index 490de2a6..3d145d96 100644
--- a/test-suite/bench/lists_100.v
+++ b/test-suite/bench/lists_100.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/test-suite/bugs/closed/2105.v b/test-suite/bugs/closed/2105.v
new file mode 100644
index 00000000..46a416fd
--- /dev/null
+++ b/test-suite/bugs/closed/2105.v
@@ -0,0 +1,2 @@
+
+Definition id (T:Type) := Eval vm_compute in T.
diff --git a/test-suite/bugs/closed/shouldfail/2406.v b/test-suite/bugs/closed/shouldfail/2406.v
new file mode 100644
index 00000000..112ea2bb
--- /dev/null
+++ b/test-suite/bugs/closed/shouldfail/2406.v
@@ -0,0 +1,3 @@
+(* Check correct handling of unsupported notations *)
+Notation "''" := (fun x => x) (at level 20).
+Definition crash_the_rooster f := .
diff --git a/test-suite/bugs/closed/shouldfail/2586.v b/test-suite/bugs/closed/shouldfail/2586.v
new file mode 100644
index 00000000..6111a641
--- /dev/null
+++ b/test-suite/bugs/closed/shouldfail/2586.v
@@ -0,0 +1,5 @@
+Require Import Setoid SetoidClass Program.
+
+Goal forall `(Setoid nat) x y, x == y -> S x == S y.
+  intros.
+  clsubst H0.
+\ No newline at end of file
diff --git a/test-suite/bugs/closed/shouldsucceed/1416.v b/test-suite/bugs/closed/shouldsucceed/1416.v
index da67d9b0..ee092005 100644
--- a/test-suite/bugs/closed/shouldsucceed/1416.v
+++ b/test-suite/bugs/closed/shouldsucceed/1416.v
@@ -1,3 +1,8 @@
+(* In 8.1 autorewrite used to raised an anomaly here *)
+(* After resolution of the bug, autorewrite succeeded *)
+(* From forthcoming 8.4, autorewrite is forbidden to instantiate *)
+(* evars, so the new test just checks it is not an anomaly *)
+
 Set Implicit Arguments.
 
 Record Place (Env A: Type) : Type := {
@@ -22,6 +27,4 @@ Lemma autorewrite_raise_anomaly: forall (Env A:Type) (e: Env) (p:Place Env A),
 Proof.
   intros Env A e p; eapply ex_intro.
   autorewrite with placeeq. (* Here is the bug *)
-  auto.
-Qed.
 
diff --git a/test-suite/bugs/closed/shouldsucceed/1507.v b/test-suite/bugs/closed/shouldsucceed/1507.v
index ea72ba89..f2ab9100 100644
--- a/test-suite/bugs/closed/shouldsucceed/1507.v
+++ b/test-suite/bugs/closed/shouldsucceed/1507.v
@@ -2,7 +2,6 @@
    Implementing reals a la Stolzenberg
 
    Danko Ilik, March 2007
-   svn revision: $Id: 1507.v 12337 2009-09-17 15:58:14Z glondu $
 
    XField.v -- (unfinished) axiomatisation of the theories of real and
                rational intervals.
diff --git a/test-suite/bugs/closed/shouldsucceed/1834.v b/test-suite/bugs/closed/shouldsucceed/1834.v
new file mode 100644
index 00000000..947d15f0
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1834.v
@@ -0,0 +1,174 @@
+(* This tests rather deep nesting of abstracted terms *)
+
+(* This used to fail before Nov 2011 because of a de Bruijn indice bug
+   in extract_predicate.
+
+   Note: use of eq_ok allows shorten notations but was not in the
+   original example
+*)
+
+Scheme eq_rec_dep := Induction for eq Sort Type.
+
+Section Teq.
+
+Variable P0:           Type.
+Variable P1: forall (y0:P0), Type.
+Variable P2: forall y0 (y1:P1 y0), Type.
+Variable P3: forall y0 y1 (y2:P2 y0 y1), Type.
+Variable P4: forall y0 y1 y2 (y3:P3 y0 y1 y2), Type.
+Variable P5: forall y0 y1 y2 y3 (y4:P4 y0 y1 y2 y3), Type.
+
+Variable x0:P0.
+
+Inductive eq0 : P0 -> Prop :=
+  refl0: eq0 x0.
+
+Definition eq_0 y0 := x0 = y0.
+
+Variable x1:P1 x0.
+
+Inductive eq1 : forall y0, P1 y0 -> Prop :=
+  refl1: eq1 x0 x1.
+
+Definition S0_0 y0 (e0:eq_0 y0) :=
+  eq_rec_dep P0 x0 (fun y0 e0 => P1 y0) x1 y0 e0.
+
+Definition eq_ok0 y0 y1 (E: eq_0 y0) := S0_0 y0 E = y1.
+
+Definition eq_1 y0 y1 :=
+  {E0:eq_0 y0 | eq_ok0 y0 y1 E0}.
+
+Variable x2:P2 x0 x1.
+
+Inductive eq2 :
+forall y0 y1, P2 y0 y1 -> Prop :=
+refl2: eq2 x0 x1 x2.
+
+Definition S1_0 y0 (e0:eq_0 y0) :=
+eq_rec_dep P0 x0 (fun y0 e0 => P2 y0 (S0_0 y0 e0)) x2 y0 e0.
+
+Definition S1_1 y0 y1 (e0:eq_0 y0) (e1:S0_0 y0 e0 = y1) :=
+  eq_rec_dep (P1 y0) (S0_0 y0 e0) (fun y1 e1 => P2 y0 y1)
+   (S1_0 y0 e0)
+   y1 e1.
+
+Definition eq_ok1 y0 y1 y2 (E: eq_1 y0 y1) :=
+  match E with exist e0 e1 => S1_1 y0 y1 e0 e1 = y2 end.
+
+Definition eq_2 y0 y1 y2 :=
+  {E1:eq_1 y0 y1 | eq_ok1 y0 y1 y2 E1}.
+
+Variable x3:P3 x0 x1 x2.
+
+Inductive eq3 :
+forall y0 y1 y2, P3 y0 y1 y2 -> Prop :=
+refl3: eq3 x0 x1 x2 x3.
+
+Definition S2_0 y0 (e0:eq_0 y0) :=
+eq_rec_dep P0 x0 (fun y0 e0 => P3 y0 (S0_0 y0 e0) (S1_0 y0 e0)) x3 y0 e0.
+
+Definition S2_1 y0 y1 (e0:eq_0 y0) (e1:S0_0 y0 e0 = y1) :=
+  eq_rec_dep (P1 y0) (S0_0 y0 e0)
+   (fun y1 e1 => P3 y0 y1 (S1_1 y0 y1 e0 e1))
+   (S2_0 y0 e0)
+   y1 e1.
+
+Definition S2_2 y0 y1 y2 (e0:eq_0 y0) (e1:S0_0 y0 e0 = y1)
+  (e2:S1_1 y0 y1 e0 e1 = y2) :=
+  eq_rec_dep (P2 y0 y1) (S1_1 y0 y1 e0 e1)
+   (fun y2 e2 => P3 y0 y1 y2)
+   (S2_1 y0 y1 e0 e1)
+   y2 e2.
+
+Definition eq_ok2 y0 y1 y2 y3 (E: eq_2 y0 y1 y2) : Prop :=
+  match E with exist (exist e0 e1) e2 =>
+     S2_2 y0 y1 y2 e0 e1 e2 = y3 end.
+
+Definition eq_3 y0 y1 y2 y3 :=
+  {E2: eq_2 y0 y1 y2 | eq_ok2 y0 y1 y2 y3 E2}.
+
+Variable x4:P4 x0 x1 x2 x3.
+
+Inductive eq4 :
+forall y0 y1 y2 y3, P4 y0 y1 y2 y3 -> Prop :=
+refl4: eq4 x0 x1 x2 x3 x4.
+
+Definition S3_0 y0 (e0:eq_0 y0) :=
+eq_rec_dep P0 x0 (fun y0 e0 => P4 y0 (S0_0 y0 e0) (S1_0 y0 e0) (S2_0 y0 e0))
+  x4 y0 e0.
+
+Definition S3_1 y0 y1 (e0:eq_0 y0) (e1:S0_0 y0 e0 = y1) :=
+  eq_rec_dep (P1 y0) (S0_0 y0 e0)
+   (fun y1 e1 => P4 y0 y1 (S1_1 y0 y1 e0 e1) (S2_1 y0 y1 e0 e1))
+   (S3_0 y0 e0)
+   y1 e1.
+
+Definition S3_2 y0 y1 y2 (e0:eq_0 y0) (e1:S0_0 y0 e0 = y1)
+  (e2:S1_1 y0 y1 e0 e1 = y2) :=
+  eq_rec_dep (P2 y0 y1) (S1_1 y0 y1 e0 e1)
+   (fun y2 e2 => P4 y0 y1 y2 (S2_2 y0 y1 y2 e0 e1 e2))
+   (S3_1 y0 y1 e0 e1)
+   y2 e2.
+
+Definition S3_3 y0 y1 y2 y3 (e0:eq_0 y0) (e1:S0_0 y0 e0 = y1)
+  (e2:S1_1 y0 y1 e0 e1 = y2) (e3:S2_2 y0 y1 y2 e0 e1 e2 = y3):=
+  eq_rec_dep (P3 y0 y1 y2) (S2_2 y0 y1 y2 e0 e1 e2)
+   (fun y3 e3 => P4 y0 y1 y2 y3)
+   (S3_2 y0 y1 y2 e0 e1 e2)
+   y3 e3.
+
+Definition eq_ok3 y0 y1 y2 y3 y4 (E: eq_3 y0 y1 y2 y3) : Prop :=
+  match E with exist (exist (exist e0 e1) e2) e3 =>
+     S3_3 y0 y1 y2 y3 e0 e1 e2 e3 = y4 end.
+
+Definition eq_4 y0 y1 y2 y3 y4 :=
+  {E3: eq_3 y0 y1 y2 y3 | eq_ok3 y0 y1 y2 y3 y4 E3}.
+
+Variable x5:P5 x0 x1 x2 x3 x4.
+
+Inductive eq5 :
+forall y0 y1 y2 y3 y4, P5 y0 y1 y2 y3 y4 -> Prop :=
+refl5: eq5 x0 x1 x2 x3 x4 x5.
+
+Definition S4_0 y0 (e0:eq_0 y0) :=
+eq_rec_dep P0 x0
+(fun y0 e0 => P5 y0 (S0_0 y0 e0) (S1_0 y0 e0) (S2_0 y0 e0) (S3_0 y0 e0))
+  x5 y0 e0.
+
+Definition S4_1 y0 y1 (e0:eq_0 y0) (e1:S0_0 y0 e0 = y1) :=
+  eq_rec_dep (P1 y0) (S0_0 y0 e0)
+   (fun y1 e1 => P5 y0 y1 (S1_1 y0 y1 e0 e1) (S2_1 y0 y1 e0 e1) (S3_1 y0 y1 e0
+e1))
+   (S4_0 y0 e0)
+   y1 e1.
+
+Definition S4_2 y0 y1 y2 (e0:eq_0 y0) (e1:S0_0 y0 e0 = y1)
+  (e2:S1_1 y0 y1 e0 e1 = y2) :=
+  eq_rec_dep (P2 y0 y1) (S1_1 y0 y1 e0 e1)
+   (fun y2 e2 => P5 y0 y1 y2 (S2_2 y0 y1 y2 e0 e1 e2) (S3_2 y0 y1 y2 e0 e1 e2))
+   (S4_1 y0 y1 e0 e1)
+   y2 e2.
+
+Definition S4_3 y0 y1 y2 y3 (e0:eq_0 y0) (e1:S0_0 y0 e0 = y1)
+  (e2:S1_1 y0 y1 e0 e1 = y2) (e3:S2_2 y0 y1 y2 e0 e1 e2 = y3):=
+  eq_rec_dep (P3 y0 y1 y2) (S2_2 y0 y1 y2 e0 e1 e2)
+   (fun y3 e3 => P5 y0 y1 y2 y3 (S3_3 y0 y1 y2 y3 e0 e1 e2 e3))
+   (S4_2 y0 y1 y2 e0 e1 e2)
+   y3 e3.
+
+Definition S4_4 y0 y1 y2 y3 y4 (e0:eq_0 y0) (e1:S0_0 y0 e0 = y1)
+  (e2:S1_1 y0 y1 e0 e1 = y2) (e3:S2_2 y0 y1 y2 e0 e1 e2 = y3)
+  (e4:S3_3 y0 y1 y2 y3 e0 e1 e2 e3 = y4) :=
+  eq_rec_dep (P4 y0 y1 y2 y3) (S3_3 y0 y1 y2 y3 e0 e1 e2 e3)
+   (fun y4 e4 => P5 y0 y1 y2 y3 y4)
+   (S4_3 y0 y1 y2 y3 e0 e1 e2 e3)
+   y4 e4.
+
+Definition eq_ok4 y0 y1 y2 y3 y4 y5 (E: eq_4 y0 y1 y2 y3 y4) : Prop :=
+  match E with exist (exist (exist (exist e0 e1) e2) e3) e4 =>
+     S4_4 y0 y1 y2 y3 y4 e0 e1 e2 e3 e4 = y5 end.
+
+Definition eq_5 y0 y1 y2 y3 y4 y5 :=
+  {E4: eq_4 y0 y1 y2 y3 y4 | eq_ok4 y0 y1 y2 y3 y4 y5 E4 }.
+
+End Teq.
diff --git a/test-suite/bugs/closed/shouldsucceed/1912.v b/test-suite/bugs/closed/shouldsucceed/1912.v
new file mode 100644
index 00000000..987a5417
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1912.v
@@ -0,0 +1,6 @@
+Require Import ZArith.
+
+Goal forall x, Z.succ (Z.pred x) = x.
+intros x.
+omega.
+Qed.
diff --git a/test-suite/bugs/closed/shouldsucceed/1962.v b/test-suite/bugs/closed/shouldsucceed/1962.v
new file mode 100644
index 00000000..a6b0fee5
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1962.v
@@ -0,0 +1,55 @@
+(* Bug 1962.v
+
+Bonjour,
+
+J'ai un exemple de lemme que j'arrivais à prouver avec fsetdec avec la 8.2beta3
+avec la beta4 et la version svn 11447 branche 8.2 çà diverge.
+
+Voici l'exemple en question, l'exmple test2 marche bien dans les deux version,
+test en revanche pose probleme:
+
+*)
+
+Require Export FSets.
+
+(** This module takes a decidable type and
+build finite sets of this type, tactics and defs *)
+
+Module BuildFSets (DecPoints: UsualDecidableType).
+
+Module Export FiniteSetsOfPoints := FSetWeakList.Make DecPoints.
+Module Export FiniteSetsOfPointsProperties :=
+ WProperties FiniteSetsOfPoints.
+Module Export Dec := WDecide FiniteSetsOfPoints.
+Module Export FM := Dec.F.
+
+Definition set_of_points := t.
+Definition Point := DecPoints.t.
+
+Definition couple(x y :Point) : set_of_points :=
+add x (add y empty).
+
+Definition triple(x y t :Point): set_of_points :=
+add x (add y (add t empty)).
+
+Lemma test : forall P A B C A' B' C',
+Equal
+(union (singleton P) (union (triple A B C) (triple A' B' C')))
+(union (triple P B B') (union (couple P A) (triple C A' C'))).
+Proof.
+intros.
+unfold triple, couple.
+Time fsetdec. (* works in 8.2 beta 3, not in beta 4 and final 8.2 *)
+              (* appears to works again in 8.3 and trunk, take 4-6 seconds *)
+Qed.
+
+Lemma test2 : forall A B C,
+Equal
+ (union (singleton C) (couple A B)) (triple A B C).
+Proof.
+intros.
+unfold triple, couple.
+Time fsetdec.
+Qed.
+
+End BuildFSets.
+\ No newline at end of file
diff --git a/test-suite/bugs/closed/shouldsucceed/2127.v b/test-suite/bugs/closed/shouldsucceed/2127.v
index 20ea4603..0fc854b6 100644
--- a/test-suite/bugs/closed/shouldsucceed/2127.v
+++ b/test-suite/bugs/closed/shouldsucceed/2127.v
@@ -6,6 +6,3 @@
 Module A.
 Hint Rewrite sym_equal using apply refl_equal : foo.
 End A.
-
-
-
diff --git a/test-suite/bugs/closed/shouldsucceed/2141.v b/test-suite/bugs/closed/shouldsucceed/2141.v
new file mode 100644
index 00000000..941ae530
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2141.v
@@ -0,0 +1,14 @@
+Require Import FSetList.
+Require Import OrderedTypeEx.
+
+Module NatSet := FSetList.Make (Nat_as_OT).
+Recursive Extraction NatSet.fold.
+
+Module FSetHide (X : FSetInterface.S).
+  Include X.
+End FSetHide.
+
+Module NatSet' := FSetHide NatSet.
+Recursive Extraction NatSet'.fold.
+
+(* Extraction "test2141.ml" NatSet'.fold. *)
+\ No newline at end of file
diff --git a/test-suite/bugs/closed/shouldsucceed/2181.v b/test-suite/bugs/closed/shouldsucceed/2181.v
new file mode 100644
index 00000000..62820d86
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2181.v
@@ -0,0 +1,3 @@
+Class C.
+Parameter P: C -> Prop.
+Fail Record R: Type := { _: C; u: P _ }.
diff --git a/test-suite/bugs/closed/shouldsucceed/2304.v b/test-suite/bugs/closed/shouldsucceed/2304.v
new file mode 100644
index 00000000..1ac2702b
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2304.v
@@ -0,0 +1,4 @@
+(* This used to fail with an anomaly NotASort at some time *)
+Class A (O: Type): Type := a: O -> Type.
+Fail Goal forall (x: a tt), @a x = @a x.
+
diff --git a/test-suite/bugs/closed/shouldsucceed/2307.v b/test-suite/bugs/closed/shouldsucceed/2307.v
new file mode 100644
index 00000000..7c049495
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2307.v
@@ -0,0 +1,3 @@
+Inductive V: nat -> Type := VS n: V (S n).
+Definition f (e: V 1): nat := match e with VS 0 => 3 end.
+
diff --git a/test-suite/bugs/closed/shouldsucceed/2320.v b/test-suite/bugs/closed/shouldsucceed/2320.v
new file mode 100644
index 00000000..facb9ecf
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2320.v
@@ -0,0 +1,14 @@
+(* Managing metavariables in the return clause of a match *)
+
+(* This was working in 8.1 but is failing in 8.2 and 8.3. It works in
+   trunk thanks to the new proof engine. It could probably made to work in
+   8.2 and 8.3 if a return predicate of the form "dummy 0" instead of
+   (or in addition to) a sophisticated predicate of the form 
+   "as x in dummy y return match y with 0 => ?P | _ => ID end" *)
+
+Inductive dummy : nat -> Prop := constr : dummy 0.
+
+Lemma failure : forall (x : dummy 0), x = constr.
+Proof.
+intros x.
+refine (match x with constr => _ end).
diff --git a/test-suite/bugs/closed/shouldsucceed/2342.v b/test-suite/bugs/closed/shouldsucceed/2342.v
new file mode 100644
index 00000000..094e5466
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2342.v
@@ -0,0 +1,8 @@
+(* Checking that the type inference algoithme does not commit to an
+   equality over sorts when only a subtyping constraint is around *)
+
+Parameter A : Set.
+Parameter B : A -> Set.
+Parameter F : Set -> Prop. 
+Check (F (forall x, B x)). 
+
diff --git a/test-suite/bugs/closed/shouldsucceed/2362.v b/test-suite/bugs/closed/shouldsucceed/2362.v
new file mode 100644
index 00000000..febb9c7b
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2362.v
@@ -0,0 +1,38 @@
+Set Implicit Arguments.
+
+Class Pointed (M:Type -> Type) := 
+{
+  creturn: forall {A: Type}, A -> M A
+}.
+
+Unset Implicit Arguments.
+Inductive FPair (A B:Type) (neutral: B) : Type:=
+ fpair : forall (a:A) (b:B), FPair A B neutral.
+Implicit Arguments fpair [[A] [B] [neutral]].
+
+Set Implicit Arguments.
+
+Notation "( x ,> y )" := (fpair x y) (at level 0).
+
+Instance Pointed_FPair B neutral:
+ Pointed (fun A => FPair A B neutral) :=
+ { creturn := fun A (a:A) => (a,> neutral) }.
+Definition blah_fail (x:bool) : FPair bool nat O :=
+  creturn x.
+Set Printing All. Print blah_fail.
+
+Definition blah_explicit (x:bool) : FPair bool nat O :=
+  @creturn _ (Pointed_FPair _ ) _ x.
+
+Print blah_explicit.
+
+
+Instance Pointed_FPair_mono:
+ Pointed (fun A => FPair A nat 0) :=
+ { creturn := fun A (a:A) => (a,> 0) }.
+
+
+Definition blah (x:bool) : FPair bool nat O :=
+  creturn x.
+
+
diff --git a/test-suite/bugs/closed/shouldsucceed/2378.v b/test-suite/bugs/closed/shouldsucceed/2378.v
new file mode 100644
index 00000000..7deec64d
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2378.v
@@ -0,0 +1,608 @@
+(* test with Coq 8.3rc1 *)
+
+Require Import Program.
+
+Inductive Unit: Set := unit: Unit.
+
+Definition eq_dec T := forall x y:T, {x=y}+{x<>y}.
+
+Section TTS_TASM.
+
+Variable Time: Set.
+Variable Zero: Time.
+Variable tle: Time -> Time -> Prop.
+Variable tlt: Time -> Time -> Prop.
+Variable tadd: Time -> Time -> Time.
+Variable tsub: Time -> Time -> Time.
+Variable tmin: Time -> Time -> Time.
+Notation "t1 @<= t2" := (tle t1 t2) (at level 70, no associativity).
+Notation "t1 @< t2" := (tlt t1 t2) (at level 70, no associativity).
+Notation "t1 @+ t2" := (tadd t1 t2) (at level 50, left associativity).
+Notation "t1 @- t2" := (tsub t1 t2) (at level 50, left associativity).
+Notation "t1 @<= t2 @<= t3" := ((tle t1 t2) /\ (tle t2 t3)) (at level 70, t2 at next level).
+Notation "t1 @<= t2 @< t3" := ((tle t1 t2) /\ (tlt t2 t3)) (at level 70, t2 at next level).
+
+Variable tzerop: forall n, (n = Zero) + {Zero @< n}.
+Variable tlt_eq_gt_dec: forall x y, {x @< y} + {x=y} + {y @< x}.
+Variable tle_plus_l: forall n m, n @<= n @+ m.
+Variable tle_lt_eq_dec: forall n m, n @<= m -> {n @< m} + {n = m}.
+
+Variable tzerop_zero: tzerop Zero = inleft (Zero @< Zero) (@eq_refl _ Zero).
+Variable tplus_n_O: forall n, n @+ Zero = n.
+Variable tlt_le_weak: forall n m, n @< m -> n @<= m.
+Variable tlt_irrefl: forall n, ~ n @< n.
+Variable tplus_nlt: forall n m, ~n @+ m @< n.
+Variable tle_n: forall n, n @<= n.
+Variable tplus_lt_compat_l: forall n m p, n @< m -> p @+ n @< p @+ m.
+Variable tlt_trans: forall n m p, n @< m -> m @< p -> n @< p.
+Variable tle_lt_trans: forall n m p, n @<= m -> m @< p -> n @< p.
+Variable tlt_le_trans: forall n m p, n @< m -> m @<= p -> n @< p.
+Variable tle_refl: forall n, n @<= n.
+Variable tplus_le_0: forall n m, n @+ m @<= n -> m = Zero.
+Variable Time_eq_dec: eq_dec Time.
+
+(*************************************************************)
+
+Section PropLogic.
+Variable Predicate: Type.
+
+Inductive LP: Type :=
+  LPPred: Predicate -> LP
+| LPAnd: LP -> LP -> LP
+| LPNot: LP -> LP.
+
+Variable State: Type.
+Variable Sat: State -> Predicate -> Prop.
+
+Fixpoint lpSat st f: Prop :=
+  match f with
+    LPPred p => Sat st p
+  | LPAnd f1 f2 => lpSat st f1 /\ lpSat st f2
+  | LPNot f1 => ~lpSat st f1
+  end.
+End PropLogic.
+
+Implicit Arguments lpSat.
+
+Fixpoint LPTransfo Pred1 Pred2 p2lp (f: LP Pred1): LP Pred2 :=
+  match f with
+    LPPred p => p2lp p
+  | LPAnd f1 f2 => LPAnd _ (LPTransfo Pred1 Pred2 p2lp f1) (LPTransfo Pred1 Pred2 p2lp f2)
+  | LPNot f1 => LPNot _ (LPTransfo Pred1 Pred2 p2lp f1)
+  end.
+Implicit Arguments LPTransfo.
+
+Definition addIndex (Ind:Type) (Pred: Ind -> Type) (i: Ind) f := 
+  LPTransfo (fun p => LPPred _ (existT (fun i => Pred i) i p)) f.
+
+Section TTS.
+
+Variable State: Type.
+
+Record TTS: Type := mkTTS {
+  Init: State -> Prop;
+  Delay: State -> Time -> State -> Prop;
+  Next: State -> State -> Prop;
+  Predicate: Type;
+  Satisfy: State -> Predicate -> Prop
+}.
+
+Definition TTSIndexedProduct Ind (tts: Ind -> TTS): TTS := mkTTS
+  (fun st => forall i, Init (tts i) st)
+  (fun st d st' => forall i, Delay (tts i) st d st')
+  (fun st st' => forall i, Next (tts i) st st')
+  { i: Ind & Predicate (tts i) }
+  (fun st p => Satisfy (tts (projT1 p)) st (projT2 p)).
+
+End TTS.
+
+Section SIMU_F.
+
+Variables StateA StateC: Type.
+
+Record mapping: Type := mkMapping {
+  mState: Type;
+  mInit: StateC -> mState;
+  mNext: mState -> StateC -> mState;
+  mDelay: mState -> StateC -> Time -> mState;
+  mabs: mState -> StateC -> StateA
+}.
+
+Variable m: mapping.
+
+Record simu (Pred: Type) (a: TTS StateA) (c: TTS StateC) (tra: Pred -> LP (Predicate _ a)) (trc: Pred -> LP (Predicate _ c)): Type := simuPrf {
+  inv: (mState m) -> StateC -> Prop;
+  invInit: forall st, Init _ c st -> inv (mInit m st) st;
+  invDelay: forall ex1 st1 st2 d, Delay _ c st1 d st2 -> inv ex1 st1 -> inv (mDelay m ex1 st1 d) st2;
+  invNext: forall ex1 st1 st2, Next _ c st1 st2 -> inv ex1 st1 -> inv (mNext m ex1 st1) st2;
+  simuInit: forall st, Init _ c st -> Init _ a (mabs m (mInit m st) st);
+  simuDelay: forall ex1 st1 st2 d, Delay _ c st1 d st2 -> inv ex1 st1 ->
+    Delay _ a (mabs m ex1 st1) d (mabs m (mDelay m ex1 st1 d) st2);
+  simuNext: forall ex1 st1 st2, Next _ c st1 st2 -> inv ex1 st1 ->
+    Next _ a (mabs m ex1 st1) (mabs m (mNext m ex1 st1) st2);
+  simuPred: forall ext st, inv ext st -> 
+    (forall p, lpSat (Satisfy _ c) st (trc p) <-> lpSat (Satisfy _ a) (mabs m ext st) (tra p)) 
+}.
+
+Theorem satProd: forall State Ind Pred (Sat: forall i, State -> Pred i -> Prop) (st:State) i (f: LP (Pred i)),
+  lpSat (Sat i) st f
+  <->
+  lpSat
+    (fun (st : State) (p : {i : Ind &  Pred i}) => Sat (projT1 p) st (projT2 p)) st
+     (addIndex Ind _ i f).
+Proof.
+  induction f; simpl; intros; split; intros; intuition.
+Qed.
+
+Definition trProd (State: Type) Ind (Pred: Ind -> Type) (tts: Ind -> TTS State) (tr: forall i, (Pred i) -> LP (Predicate _ (tts i))):
+  {i:Ind & Pred i} -> LP (Predicate _ (TTSIndexedProduct _ Ind tts)) :=
+  fun p => addIndex Ind _ (projS1 p) (tr (projS1 p) (projS2 p)).
+
+Implicit Arguments trProd.
+Require Import Setoid.
+
+Theorem satTrProd:
+  forall State Ind Pred (tts: Ind -> TTS State) 
+    (tr: forall i, (Pred  i) -> LP (Predicate _ (tts i))) (st:State) (p: {i:Ind & (Pred i)}),
+  lpSat (Satisfy _ (tts (projS1 p))) st (tr (projS1 p) (projS2 p))
+  <->
+  lpSat (Satisfy _ (TTSIndexedProduct _ _ tts)) st (trProd _ tts tr p).
+Proof.
+  unfold trProd, TTSIndexedProduct; simpl; intros.
+  rewrite (satProd State Ind (fun i => Predicate State (tts i))
+                      (fun i => Satisfy _ (tts i))); tauto.
+Qed.
+
+Theorem simuProd: 
+  forall Ind (Pred: Ind -> Type) (tta: Ind -> TTS StateA) (ttc: Ind -> TTS StateC) 
+    (tra: forall i, (Pred i) -> LP (Predicate _ (tta i)))
+    (trc: forall i, (Pred i) -> LP (Predicate _ (ttc i))),
+     (forall i, simu _ (tta i) (ttc i) (tra i) (trc i)) -> 
+       simu _ (TTSIndexedProduct _ Ind tta) (TTSIndexedProduct _ Ind ttc)
+                  (trProd Pred tta tra) (trProd Pred ttc trc).
+Proof.
+  intros.
+  apply simuPrf with (fun ex st => forall i, inv _ _ (ttc i) (tra i) (trc i) (X i) ex st); simpl; intros; auto.
+  eapply invInit; eauto.
+  eapply invDelay; eauto.
+  eapply invNext; eauto.
+  eapply simuInit; eauto.
+  eapply simuDelay; eauto.
+  eapply simuNext; eauto.
+  split; simpl; intros.
+  generalize (proj1 (simuPred _ _ _ _ _ (X (projS1 p)) ext st (H (projS1 p)) (projS2 p))); simpl; intro.
+  rewrite <- (satTrProd StateA Ind Pred tta tra); apply H1.
+  rewrite (satTrProd StateC Ind Pred ttc trc); apply H0.
+
+  generalize (proj2 (simuPred _ _ _ _ _ (X (projS1 p)) ext st (H (projS1 p)) (projS2 p))); simpl; intro.
+  rewrite <- (satTrProd StateC Ind Pred ttc trc); apply H1.
+  rewrite (satTrProd StateA Ind Pred tta tra); apply H0.
+Qed.
+
+End SIMU_F.
+
+Section TRANSFO.
+
+Record simu_equiv StateA StateC m1 m2 Pred (a: TTS StateA) (c: TTS StateC) (tra: Pred -> LP (Predicate _ a)) (trc: Pred -> LP (Predicate _ c)): Type := simuEquivPrf {
+  simuLR: simu StateA StateC m1 Pred a c tra trc;
+  simuRL: simu StateC StateA m2 Pred c a trc tra
+}.
+
+Theorem simu_equivProd: 
+  forall StateA StateC m1 m2 Ind (Pred: Ind -> Type) (tta: Ind -> TTS StateA) (ttc: Ind -> TTS StateC) 
+    (tra: forall i, (Pred i) -> LP (Predicate _ (tta i)))
+    (trc: forall i, (Pred i) -> LP (Predicate _ (ttc i))),
+     (forall i, simu_equiv StateA StateC m1 m2 _ (tta i) (ttc i) (tra i) (trc i)) -> 
+       simu_equiv StateA StateC m1 m2 _ (TTSIndexedProduct _ Ind tta) (TTSIndexedProduct _ Ind ttc)
+                  (trProd _ _ Pred tta tra) (trProd _ _ Pred ttc trc).
+Proof.
+  intros; split; intros.
+  apply simuProd; intro.
+  elim (X i); auto.
+  apply simuProd; intro.
+  elim (X i); auto.
+Qed.
+
+Record RTLanguage: Type := mkRTLanguage {
+   Syntax: Type;
+   DynamicState: Syntax -> Type;
+   Semantic: forall (mdl:Syntax), TTS (DynamicState mdl);
+   MdlPredicate: Syntax -> Type;
+   MdlPredicateDefinition: forall mdl, MdlPredicate mdl -> LP (Predicate _ (Semantic mdl))
+}.
+
+Record Transformation (l1 l2: RTLanguage): Type := mkTransformation {
+  Tmodel: Syntax l1 -> Syntax l2;
+  Tl1l2: forall mdl, mapping (DynamicState l1 mdl) (DynamicState l2 (Tmodel mdl));
+  Tl2l1: forall mdl, mapping (DynamicState l2 (Tmodel mdl)) (DynamicState l1 mdl);
+  Tpred: forall mdl, MdlPredicate l1 mdl -> LP (MdlPredicate l2 (Tmodel mdl));
+  Tsim: forall mdl, simu_equiv (DynamicState l1 mdl) (DynamicState l2 (Tmodel mdl)) (Tl1l2 mdl) (Tl2l1 mdl)
+    (MdlPredicate l1 mdl) (Semantic l1 mdl) (Semantic l2 (Tmodel mdl))
+    (MdlPredicateDefinition l1 mdl)
+    (fun p => LPTransfo (MdlPredicateDefinition l2 (Tmodel mdl)) (Tpred mdl p))
+}.
+
+Section Product.
+
+Record PSyntax (L: RTLanguage): Type := mkPSyntax {
+  pIndex: Type;
+  pIsEmpty: pIndex + {pIndex -> False};
+  pState: Type;
+  pComponents: pIndex -> Syntax L;
+  pIsShared: forall i, DynamicState L (pComponents i) = pState
+}.
+
+Definition pPredicate (L: RTLanguage) (sys: PSyntax L) := { i : pIndex L sys & MdlPredicate L (pComponents L sys i)}.
+
+(* product with shared state *)
+
+Definition PLanguage (L: RTLanguage): RTLanguage := 
+  mkRTLanguage
+    (PSyntax L)
+    (pState L)
+    (fun mdl => TTSIndexedProduct (pState L mdl) (pIndex L mdl)
+      (fun i => match pIsShared L mdl i in (_ = y) return TTS y with
+        eq_refl => Semantic L (pComponents L mdl i)
+       end))
+    (pPredicate L)
+    (fun mdl => trProd _ _ _ _ 
+      (fun i pi => match pIsShared L mdl i as e in (_ = y) return
+                     (LP (Predicate y
+                               match e in (_ = y0) return (TTS y0) with
+                               | eq_refl => Semantic L (pComponents L mdl i)
+                               end))
+     with
+     | eq_refl => MdlPredicateDefinition L (pComponents L mdl i) pi
+     end)).
+
+Inductive Empty: Type :=.
+
+Record isSharedTransfo l1 l2 tr: Prop := isSharedTransfoPrf {
+sameState:  forall mdl i j, 
+  DynamicState l2 (Tmodel l1 l2 tr (pComponents l1 mdl i)) =
+  DynamicState l2 (Tmodel l1 l2 tr (pComponents l1 mdl j));
+sameMState: forall mdl i j, 
+  mState _ _  (Tl1l2 _ _ tr (pComponents l1 mdl i)) =
+  mState _ _  (Tl1l2 _ _ tr (pComponents l1 mdl j));
+sameM12: forall mdl i j, 
+  Tl1l2 _ _ tr (pComponents l1 mdl i) =
+  match sym_eq (sameState mdl i j) in _=y return mapping _ y with
+    eq_refl => match sym_eq (pIsShared l1 mdl i) in _=x return mapping x _ with
+      eq_refl => match pIsShared l1 mdl j in _=x return mapping x _ with
+        eq_refl => Tl1l2 _ _ tr (pComponents l1 mdl j)
+      end
+    end         
+  end;
+sameM21: forall mdl i j, 
+  Tl2l1 l1 l2 tr (pComponents l1 mdl i) =
+  match
+    sym_eq (sameState mdl i j) in (_ = y)
+    return (mapping y (DynamicState l1 (pComponents l1 mdl i)))
+  with eq_refl =>
+    match
+      sym_eq (pIsShared l1 mdl i) in (_ = y)
+      return
+        (mapping (DynamicState l2 (Tmodel l1 l2 tr (pComponents l1 mdl j))) y)
+    with
+    | eq_refl =>
+        match
+          pIsShared l1 mdl j in (_ = y)
+          return
+            (mapping
+               (DynamicState l2 (Tmodel l1 l2 tr (pComponents l1 mdl j))) y)
+        with
+        | eq_refl => Tl2l1 l1 l2 tr (pComponents l1 mdl j)
+        end
+    end
+end
+}.
+
+Definition PTransfoSyntax l1 l2 tr (h: isSharedTransfo l1 l2 tr) mdl :=
+  mkPSyntax l2 (pIndex l1 mdl)
+    (pIsEmpty l1 mdl)
+    (match pIsEmpty l1 mdl return Type with 
+         inleft i => DynamicState l2 (Tmodel l1 l2 tr (pComponents l1 mdl i))
+        |inright h => pState l1 mdl
+       end)
+    (fun i => Tmodel l1 l2 tr (pComponents l1 mdl i))
+    (fun i => match pIsEmpty l1 mdl as y return
+        (DynamicState l2 (Tmodel l1 l2 tr (pComponents l1 mdl i)) =
+         match y with
+         | inleft i0 =>
+             DynamicState l2 (Tmodel l1 l2 tr (pComponents l1 mdl i0))
+         | inright _ => pState l1 mdl
+         end)
+      with
+         inleft j => sameState l1 l2 tr h mdl i j 
+      | inright h => match h i with end
+        end).
+
+Definition compSemantic l mdl i :=
+    match pIsShared l mdl i in (_=y) return TTS y with
+        eq_refl => Semantic l (pComponents l mdl i)
+    end.
+
+Definition compSemanticEq l mdl i s (e: DynamicState l (pComponents l mdl i) = s) :=
+    match e in (_=y) return TTS y with
+        eq_refl => Semantic l (pComponents l mdl i)
+    end.
+
+Definition Pmap12 l1 l2 tr (h: isSharedTransfo l1 l2 tr) (mdl : PSyntax l1) :=
+match
+  pIsEmpty l1 mdl as s
+  return
+    (mapping (pState l1 mdl)
+       match s with
+       | inleft i => DynamicState l2 (Tmodel l1 l2 tr (pComponents l1 mdl i))
+       | inright _ => pState l1 mdl
+       end)
+with
+| inleft p =>
+    match
+      pIsShared l1 mdl p in (_ = y)
+      return
+        (mapping y (DynamicState l2 (Tmodel l1 l2 tr (pComponents l1 mdl p))))
+    with
+    | eq_refl => Tl1l2 l1 l2 tr (pComponents l1 mdl p)
+    end
+| inright _ =>
+    mkMapping (pState l1 mdl) (pState l1 mdl) Unit
+      (fun _ : pState l1 mdl => unit)
+      (fun (_ : Unit) (_ : pState l1 mdl) => unit)
+      (fun (_ : Unit) (_ : pState l1 mdl) (_ : Time) => unit)
+      (fun (_ : Unit) (X : pState l1 mdl) => X)
+end.
+
+Definition Pmap21 l1 l2 tr (h : isSharedTransfo l1 l2 tr) mdl :=
+match
+  pIsEmpty l1 mdl as s
+  return
+    (mapping
+       match s with
+       | inleft i => DynamicState l2 (Tmodel l1 l2 tr (pComponents l1 mdl i))
+       | inright _ => pState l1 mdl
+       end (pState l1 mdl))
+with
+| inleft p =>
+    match
+      pIsShared l1 mdl p in (_ = y)
+      return
+        (mapping (DynamicState l2 (Tmodel l1 l2 tr (pComponents l1 mdl p))) y)
+    with
+    | eq_refl => Tl2l1 l1 l2 tr (pComponents l1 mdl p)
+    end
+| inright _ =>
+    mkMapping (pState l1 mdl) (pState l1 mdl) Unit
+      (fun _ : pState l1 mdl => unit)
+      (fun (_ : Unit) (_ : pState l1 mdl) => unit)
+      (fun (_ : Unit) (_ : pState l1 mdl) (_ : Time) => unit)
+      (fun (_ : Unit) (X : pState l1 mdl) => X)
+end.
+
+Definition PTpred l1 l2 tr (h : isSharedTransfo l1 l2 tr) mdl (pp : pPredicate l1 mdl):
+  LP (MdlPredicate (PLanguage l2) (PTransfoSyntax l1 l2 tr h mdl)) :=
+match pIsEmpty l1 mdl with
+| inleft _ =>
+      let (x, p) := pp in
+      addIndex (pIndex l1 mdl) (fun i => MdlPredicate l2 (Tmodel l1 l2 tr (pComponents l1 mdl i))) x
+        (LPTransfo (Tpred l1 l2 tr (pComponents l1 mdl x))
+          (LPPred (MdlPredicate l1 (pComponents l1 mdl x)) p))
+| inright f => match f (projS1 pp) with end
+end.
+
+Lemma simu_eqA: 
+  forall A1 A2 C m P sa sc tta ttc (h: A2=A1),
+  simu A1 C (match h in (_=y) return mapping _ C with eq_refl => m end) 
+  P (match h in (_=y) return TTS y with eq_refl => sa end)
+  sc (fun p => match h in (_=y) return LP (Predicate y _) with eq_refl => tta p end)
+  ttc ->
+  simu A2 C m P sa sc tta ttc.
+admit.
+Qed.
+
+Lemma simu_eqC: 
+  forall A C1 C2 m P sa sc tta ttc (h: C2=C1),
+  simu A C1 (match h in (_=y) return mapping A _ with eq_refl => m end) 
+  P sa (match h in (_=y) return TTS y with eq_refl => sc end)
+  tta (fun p => match h in (_=y) return LP (Predicate y _) with eq_refl => ttc p end)
+   ->
+  simu A C2 m P sa sc tta ttc.
+admit.
+Qed.
+
+Lemma simu_eqA1: 
+  forall A1 A2 C m P sa sc tta ttc (h: A1=A2),
+  simu A1 C m 
+  P 
+  (match (sym_eq h) in (_=y) return TTS y with eq_refl => sa end) sc
+  (fun p => match (sym_eq h) as e in (_=y) return LP (Predicate y (match e in (_=z) return TTS z with eq_refl => sa end)) with eq_refl => tta p end) ttc
+   ->
+  simu A2 C (match h in (_=y) return mapping _ C with eq_refl => m end) P sa sc tta ttc.
+admit.
+Qed.
+
+Lemma simu_eqA2: 
+  forall A1 A2 C m P sa sc tta ttc (h: A1=A2),
+  simu A1 C (match (sym_eq h) in (_=y) return mapping _ C with eq_refl => m end)
+  P 
+  sa sc tta ttc
+   ->
+  simu A2 C m P
+  (match h in (_=y) return TTS y with eq_refl => sa end) sc 
+  (fun p => match h as e in (_=y) return LP (Predicate y match e in (_=y0) return TTS y0 with eq_refl => sa end) with eq_refl => tta p end)
+ ttc.
+admit.
+Qed.
+
+Lemma simu_eqC2: 
+  forall A C1 C2 m P sa sc tta ttc (h: C1=C2),
+  simu A C1 (match (sym_eq h) in (_=y) return mapping A _ with eq_refl => m end)
+  P 
+  sa sc tta ttc
+   ->
+  simu A C2 m P
+  sa (match h in (_=y) return TTS y with eq_refl => sc end) 
+  tta (fun p => match h as e in (_=y) return LP (Predicate y match e in (_=y0) return TTS y0 with eq_refl => sc end) with eq_refl => ttc p end).
+admit.
+Qed.
+
+Lemma simu_eqM: 
+  forall A C m1 m2 P sa sc tta ttc (h: m1=m2),
+  simu A C m1 P sa sc tta ttc
+   ->
+  simu A C m2 P sa sc tta ttc.
+admit.
+Qed.
+
+Lemma LPTransfo_trans:
+  forall Pred1 Pred2 Pred3 (tr1: Pred1 -> LP Pred2) (tr2: Pred2 -> LP Pred3) f,
+    LPTransfo tr2 (LPTransfo tr1 f) = LPTransfo (fun x => LPTransfo tr2 (tr1 x)) f.
+Proof.
+  admit.
+Qed.
+
+Lemma LPTransfo_addIndex:
+  forall Ind Pred tr1 x (tr2: forall i, Pred i -> LP (tr1 i)) (p: LP (Pred x)),
+    addIndex Ind tr1 x (LPTransfo (tr2 x) p) =
+    LPTransfo
+      (fun p0 : {i : Ind & Pred i} =>
+        addIndex Ind tr1 (projT1 p0) (tr2 (projT1 p0) (projT2 p0)))
+      (addIndex Ind Pred x p).
+Proof.
+  unfold addIndex; intros. 
+  rewrite LPTransfo_trans.
+  rewrite LPTransfo_trans.
+  simpl.
+  auto.
+Qed.
+
+Record tr_compat I0 I1 tr := compatPrf {
+  and_compat: forall p1 p2, tr (LPAnd I0 p1 p2) = LPAnd I1 (tr p1) (tr p2);
+  not_compat: forall p, tr (LPNot I0 p) = LPNot I1 (tr p)
+}.
+
+Lemma LPTransfo_addIndex_tr:
+  forall Ind Pred tr0 tr1 x (tr2: forall i, Pred i -> LP (tr0 i))  (tr3: forall i, LP (tr0 i) -> LP (tr1 i)) (p: LP (Pred x)),
+    (forall x, tr_compat (tr0 x) (tr1 x) (tr3 x)) ->
+    addIndex Ind tr1 x (tr3 x (LPTransfo (tr2 x) p)) =
+    LPTransfo
+      (fun p0 : {i : Ind & Pred i} =>
+        addIndex Ind tr1 (projT1 p0) (tr3 (projT1 p0) (tr2 (projT1 p0) (projT2 p0))))
+      (addIndex Ind Pred x p).
+Proof.
+  unfold addIndex; simpl; intros. 
+  rewrite LPTransfo_trans; simpl.
+  rewrite <- LPTransfo_trans.
+  f_equal.
+  induction p; simpl; intros; auto.
+  rewrite (and_compat _ _ _ (H x)).
+  rewrite <- IHp1, <- IHp2; auto.
+  rewrite <- IHp.
+  rewrite (not_compat _ _ _ (H x)); auto.
+Qed.
+
+Require Export Coq.Logic.FunctionalExtensionality.
+Print PLanguage.
+Program Definition PTransfo l1 l2 (tr: Transformation l1 l2) (h: isSharedTransfo l1 l2 tr): 
+Transformation (PLanguage l1) (PLanguage l2) :=
+  mkTransformation (PLanguage l1) (PLanguage l2)
+    (PTransfoSyntax l1 l2 tr h)
+    (Pmap12 l1 l2 tr h)
+    (Pmap21 l1 l2 tr h)
+    (PTpred l1 l2 tr h)
+    (fun mdl => simu_equivProd 
+      (pState l1 mdl) 
+      (pState l2 (PTransfoSyntax l1 l2 tr h mdl)) 
+      (Pmap12 l1 l2 tr h mdl)
+      (Pmap21 l1 l2 tr h mdl)
+      (pIndex l1 mdl) 
+      (fun i => MdlPredicate l1 (pComponents l1 mdl i))
+      (compSemantic l1 mdl)
+      (compSemantic l2 (PTransfoSyntax l1 l2 tr h mdl))
+      _
+      _
+      _
+        ).
+
+Next Obligation.
+  unfold compSemantic, PTransfoSyntax; simpl.
+  case (pIsEmpty l1 mdl); simpl; intros.
+  unfold pPredicate; simpl.
+  unfold pPredicate in X; simpl in X.
+  case (sameState l1 l2 tr h mdl i p).
+  apply (LPTransfo (MdlPredicateDefinition l2 (Tmodel l1 l2 tr (pComponents l1 mdl i)))).
+  apply (LPTransfo (Tpred l1 l2 tr (pComponents l1 mdl i))).
+  apply (LPPred _ X).
+
+  apply False_rect; apply (f i).
+Defined.
+
+Next Obligation.
+  split; intros.
+  unfold Pmap12; simpl.
+  unfold PTransfo_obligation_1; simpl.
+  unfold compSemantic; simpl.
+  unfold eq_ind, eq_rect, f_equal; simpl.
+  case (pIsEmpty l1 mdl); intros.
+  apply simu_eqA2.
+  apply simu_eqC2.
+  apply simu_eqM with (Tl1l2 l1 l2 tr (pComponents l1 mdl i)).
+  apply sameM12.
+  apply (simuLR _ _ _ _ _ _ _ _ _ (Tsim l1 l2 tr (pComponents l1 mdl i))); intro.
+
+  apply False_rect; apply (f i).
+
+  unfold Pmap21; simpl.
+  unfold PTransfo_obligation_1; simpl.
+  unfold compSemantic; simpl.
+  unfold eq_ind, eq_rect, f_equal; simpl.
+  case (pIsEmpty l1 mdl); intros.
+  apply simu_eqC2.
+  apply simu_eqA2.
+  apply simu_eqM with (Tl2l1 l1 l2 tr (pComponents l1 mdl i)).
+  apply sameM21.
+  apply (simuRL _ _ _ _ _ _ _ _ _ (Tsim l1 l2 tr (pComponents l1 mdl i))); intro.
+
+  apply False_rect; apply (f i).
+Qed.
+
+Next Obligation.
+  unfold trProd; simpl.
+  unfold PTransfo_obligation_1; simpl.
+  unfold compSemantic; simpl.
+  unfold eq_ind, eq_rect, f_equal; simpl.
+  apply functional_extensionality; intro.
+  case x; clear x; intros.
+  unfold PTpred; simpl.
+  case (pIsEmpty l1 mdl); simpl; intros.
+  set (tr0 i :=
+   Predicate (DynamicState l2 (Tmodel l1 l2 tr (pComponents l1 mdl i)))
+     (Semantic l2 (Tmodel l1 l2 tr (pComponents l1 mdl i)))).
+  set (tr1 i :=
+   Predicate (DynamicState l2 (Tmodel l1 l2 tr (pComponents l1 mdl p)))
+     match sameState l1 l2 tr h mdl i p in (_ = y) return (TTS y) with
+     | eq_refl => Semantic l2 (Tmodel l1 l2 tr (pComponents l1 mdl i))
+     end).
+  set (tr2 x := MdlPredicateDefinition l2 (Tmodel l1 l2 tr (pComponents l1 mdl x))).
+  set (Pred x := MdlPredicate l2 (Tmodel l1 l2 tr (pComponents l1 mdl x))).
+  set (tr3 x f := match
+    sameState l1 l2 tr h mdl x p as e in (_ = y)
+    return
+      (LP
+         (Predicate y
+            match e in (_ = y0) return (TTS y0) with
+            | eq_refl => Semantic l2 (Tmodel l1 l2 tr (pComponents l1 mdl x))
+            end))
+  with
+  | eq_refl => f
+  end).
+  apply (LPTransfo_addIndex_tr _ Pred tr0 tr1 x tr2 tr3
+    (Tpred l1 l2 tr (pComponents l1 mdl x) m)).
+  unfold tr0, tr1, tr3; intros; split; simpl; intros; auto.
+  case (sameState l1 l2 tr h mdl x0 p); auto.
+  case (sameState l1 l2 tr h mdl x0 p); auto.
+
+  apply False_rect; apply (f x).
+Qed.
+
+End Product.
diff --git a/test-suite/bugs/closed/shouldsucceed/2388.v b/test-suite/bugs/closed/shouldsucceed/2388.v
index 8cc43ee6..c7926711 100644
--- a/test-suite/bugs/closed/shouldsucceed/2388.v
+++ b/test-suite/bugs/closed/shouldsucceed/2388.v
@@ -2,3 +2,9 @@
 
 Fail Parameters (A:Prop) (a:A A).
 
+(* This is a variant (reported as part of bug #2347) *)
+
+Require Import EquivDec.                                              
+Fail Program Instance bool_eq_eqdec : EqDec bool eq := 
+   {equiv_dec x y := (fix aux (x y : bool) {struct x}:= aux _ y) x y}.
+
diff --git a/test-suite/bugs/closed/shouldsucceed/2393.v b/test-suite/bugs/closed/shouldsucceed/2393.v
new file mode 100644
index 00000000..fb4f9261
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2393.v
@@ -0,0 +1,13 @@
+Require Import Program.
+
+Inductive T := MkT.
+
+Definition sizeOf (t : T) : nat
+    := match t with
+       | MkT => 1
+       end.
+Variable vect : nat -> Type.
+Program Fixpoint idType (t : T) (n := sizeOf t) (b : vect n) {measure n} : T
+    := match t with
+       | MkT => MkT
+       end.
diff --git a/test-suite/bugs/closed/shouldsucceed/2404.v b/test-suite/bugs/closed/shouldsucceed/2404.v
new file mode 100644
index 00000000..fe8eba54
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2404.v
@@ -0,0 +1,46 @@
+(* Check that dependencies in the indices of the type of the terms to
+   match are taken into account and correctly generalized *)
+
+Require Import Relations.Relation_Definitions.
+Require Import Basics.
+
+Record Base := mkBase
+ {(* Primitives *)
+    World : Set
+  (* Names are real, links are theoretical *)
+  ; Name : World -> Set
+
+  ; wweak : World -> World -> Prop
+
+  ; exportw : forall a b : World, (wweak a b) -> (Name b) -> option (Name a)
+}.
+
+Section Derived.
+  Variable base : Base.
+  Definition bWorld := World base.
+  Definition bName  := Name base.
+  Definition bexportw := exportw base.
+  Definition bwweak := wweak base.
+
+  Implicit Arguments bexportw [a b].
+
+Inductive RstarSetProof {I : Type} (T : I -> I -> Type) : I -> I -> Type :=
+  starReflS : forall a, RstarSetProof T a a
+| starTransS : forall i j k, T i j -> (RstarSetProof T j k) -> RstarSetProof T i k.
+
+Implicit Arguments starTransS [I T i j k].
+
+Definition RstarInv {A : Set} (rel : relation A) : A -> A -> Type :=  (flip (RstarSetProof (flip rel))).
+
+Definition bwweakFlip (b a : bWorld) : Prop := (bwweak a b).
+Definition Rweak : forall a b : bWorld, Type := RstarInv bwweak.
+
+Fixpoint exportRweak {a b} (aRWb : Rweak a b) (y : bName b) : option (bName a) :=
+  match aRWb,y with
+  | starReflS a, y' => Some y'
+  | starTransS i j k jWk jRWi, y' =>
+    match (bexportw jWk y) with
+    | Some x => exportRweak jRWi x
+    | None   => None
+    end
+  end.
diff --git a/test-suite/bugs/closed/shouldsucceed/2456.v b/test-suite/bugs/closed/shouldsucceed/2456.v
new file mode 100644
index 00000000..56f046c4
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2456.v
@@ -0,0 +1,53 @@
+
+Require Import Equality.
+
+Parameter Patch : nat -> nat -> Set.
+
+Inductive Catch (from to : nat) : Type
+    := MkCatch : forall (p : Patch from to),
+                 Catch from to.
+Implicit Arguments MkCatch [from to].
+
+Inductive CatchCommute5
+        : forall {from mid1 mid2 to : nat},
+          Catch from mid1
+       -> Catch mid1 to
+       -> Catch from mid2
+       -> Catch mid2 to
+       -> Prop
+     := MkCatchCommute5 :
+           forall {from mid1 mid2 to : nat}
+                  (p : Patch from mid1)
+                  (q : Patch mid1 to)
+                  (q' : Patch from mid2)
+                  (p' : Patch mid2 to),
+           CatchCommute5 (MkCatch p) (MkCatch q) (MkCatch q') (MkCatch p').
+
+Inductive CatchCommute {from mid1 mid2 to : nat}
+                       (p : Catch from mid1)
+                       (q : Catch mid1 to)
+                       (q' : Catch from mid2)
+                       (p' : Catch mid2 to)
+                     : Prop
+    := isCatchCommute5 : forall (catchCommuteDetails : CatchCommute5 p q q' p'),
+                         CatchCommute p q q' p'.
+Notation "<< p , q >> <~> << q' , p' >>"
+    := (CatchCommute p q q' p')
+    (at level 60, no associativity).
+
+Lemma CatchCommuteUnique2 :
+      forall {from mid mid' to : nat}
+             {p   : Catch from mid}  {q   : Catch mid  to}
+             {q'  : Catch from mid'} {p'  : Catch mid' to}
+             {q'' : Catch from mid'} {p'' : Catch mid' to}
+             (commute1 : <<p, q>> <~> <<q', p'>>)
+             (commute2 : <<p, q>> <~> <<q'', p''>>),
+      (p' = p'') /\ (q' = q'').
+Proof with auto.
+intros.
+set (X := commute2).
+dependent destruction commute1;
+dependent destruction catchCommuteDetails;
+dependent destruction commute2;
+dependent destruction catchCommuteDetails generalizing X.
+Admitted.
+\ No newline at end of file
diff --git a/test-suite/bugs/closed/shouldsucceed/2473.v b/test-suite/bugs/closed/shouldsucceed/2473.v
new file mode 100644
index 00000000..4c302512
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2473.v
@@ -0,0 +1,39 @@
+
+Require Import Relations Program Setoid Morphisms.
+
+Section S1.
+  Variable R: nat -> relation bool.
+  Instance HR1: forall n, Transitive (R n). Admitted.
+  Instance HR2: forall n, Symmetric (R n).  Admitted.
+  Hypothesis H: forall n a, R n (andb a a) a.
+  Goal forall n a b, R n b a.
+   intros. 
+   (* rewrite <- H. *) (* Anomaly: Evar ?.. was not declared. Please report. *)
+   (* idem with setoid_rewrite *)
+(*    assert (HR2' := HR2 n). *)
+   rewrite <- H.                (* ok *)
+   admit.
+  Qed.
+End S1.
+
+Section S2.
+  Variable R: nat -> relation bool.
+  Instance HR: forall n, Equivalence (R n). Admitted.
+  Hypothesis H: forall n a, R n (andb a a) a.
+  Goal forall n a b, R n a b.
+   intros. rewrite <- H. admit.
+  Qed.
+End S2.
+
+(* the parametrised relation is required to get the problem *)
+Section S3.
+  Variable R: relation bool.
+  Instance HR1': Transitive R. Admitted.
+  Instance HR2': Symmetric R.  Admitted.
+  Hypothesis H: forall a, R (andb a a) a.
+  Goal forall a b, R b a.
+   intros. 
+   rewrite <- H.                (* ok *)
+   admit.
+  Qed.
+End S3.
+\ No newline at end of file
diff --git a/test-suite/bugs/closed/shouldsucceed/2603.v b/test-suite/bugs/closed/shouldsucceed/2603.v
new file mode 100644
index 00000000..a556b9bf
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2603.v
@@ -0,0 +1,18 @@
+Module Type T.
+End T.
+
+Declare Module K : T.
+
+Module Type L.
+Declare Module E : T.
+End L.
+
+Module M1 : L with Module E:=K.
+Module E := K.
+Fail Inductive t := E. (* Used to be accepted, but End M1 below was failing *)
+End M1.
+
+Module M2 : L with Module E:=K.
+Inductive t := E.
+Fail Module E := K. (* Used to be accepted *)
+Fail End M2. (* Used to be accepted *)
diff --git a/test-suite/bugs/closed/shouldsucceed/2613.v b/test-suite/bugs/closed/shouldsucceed/2613.v
new file mode 100644
index 00000000..4f0470b1
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2613.v
@@ -0,0 +1,17 @@
+(* Check that eq_sym is still pointing to Logic.eq_sym after use of Function *)
+
+Require Import ZArith.
+Require Recdef.
+
+Axiom nat_eq_dec: forall x y : nat, {x=y}+{x<>y}.
+
+Locate eq_sym.  (* Constant Coq.Init.Logic.eq_sym  *)
+
+Function loop (n: nat) {measure (fun x => x) n} : bool :=
+  if nat_eq_dec n 0 then false else loop (pred n).
+Proof.
+   admit.
+Defined.
+
+Check eq_sym eq_refl : 0=0.
+
diff --git a/test-suite/bugs/closed/shouldsucceed/2615.v b/test-suite/bugs/closed/shouldsucceed/2615.v
new file mode 100644
index 00000000..54e1a07c
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2615.v
@@ -0,0 +1,14 @@
+(* This failed with an anomaly in pre-8.4 because of let-in not
+   properly taken into account in the test for unification pattern *)
+
+Inductive foo : forall A, A -> Prop :=
+| foo_intro : forall A x, foo A x.
+Lemma bar A B f : foo (A -> B) f -> forall x : A, foo B (f x).
+Fail induction 1.
+
+(* Whether these examples should succeed with a non-dependent return predicate 
+   or fail because there is well-typed return predicate dependent in f 
+   is questionable. As of 25 oct 2011, they succeed *)
+refine (fun p => match p with _ => _ end).
+Undo.
+refine (fun p => match p with foo_intro _ _ => _ end).
diff --git a/test-suite/bugs/closed/shouldsucceed/2616.v b/test-suite/bugs/closed/shouldsucceed/2616.v
new file mode 100644
index 00000000..8758e32d
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2616.v
@@ -0,0 +1,7 @@
+(* Testing ill-typed rewrite which used to succeed in 8.3 *)
+Goal 
+  forall (N : nat -> Prop) (g : nat -> sig N) (IN : forall a : sig N, a = g 0), 
+    N 0 -> False.
+Proof.
+intros.
+Fail rewrite IN in H.
diff --git a/test-suite/bugs/closed/shouldsucceed/2640.v b/test-suite/bugs/closed/shouldsucceed/2640.v
new file mode 100644
index 00000000..da0cc68a
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2640.v
@@ -0,0 +1,17 @@
+(* Testing consistency of globalization and interpretation in some
+   extreme cases *)
+
+Section sect.
+
+  (* Simplification of the initial example *)
+  Hypothesis Other: True.
+
+  Lemma C2 : True.
+  proof.
+  Fail have True using Other.
+  Abort.
+
+  (* Variant of the same problem *)
+  Lemma C2 : True.
+  Fail clear; Other.
+  Abort.
diff --git a/test-suite/bugs/opened/shouldnotfail/2310.v b/test-suite/bugs/opened/shouldnotfail/2310.v
new file mode 100644
index 00000000..8d1a5149
--- /dev/null
+++ b/test-suite/bugs/opened/shouldnotfail/2310.v
@@ -0,0 +1,17 @@
+(* Dependent higher-order hole in "refine" (simplified version) *)
+
+Set Implicit Arguments.
+
+Inductive Nest t := Cons : Nest (prod t t) -> Nest t.
+
+Definition cast A x y Heq P H := @eq_rect A x P H y Heq.
+
+Definition replace a (y:Nest (prod a a)) : a = a -> Nest a.
+
+(* This used to raise an anomaly Unknown Meta in 8.2 and 8.3beta.
+   It raises a regular error in 8.3 and almost succeeds with the new
+   proof engine: there are two solutions to a unification problem
+   (P:=\a.Nest (prod a a) and P:=\_.Nest (prod a a)) and refine should either
+   leave P as subgoal or choose itself one solution *)
+
+intros. refine (Cons (cast H _ y)).
diff --git a/test-suite/complexity/Notations.v b/test-suite/complexity/Notations.v
new file mode 100644
index 00000000..02a3c252
--- /dev/null
+++ b/test-suite/complexity/Notations.v
@@ -0,0 +1,10 @@
+(* Last line should not loop, even in the presence of eta-expansion in the *)
+(* printing mechanism *)
+(* Expected time < 1.00s *)
+
+Notation "'bind' x <- y ; z" :=(y (fun x => z)) (at level 99, x at
+  level 0, y at level 0,format "'[hv' 'bind'  x  <-  y ;  '/' z ']'").
+
+Definition f (g : (nat -> nat) -> nat) := g (fun x => 0).
+
+Time Check (fun g => f g).
diff --git a/test-suite/complexity/evar_instance.v b/test-suite/complexity/evar_instance.v
new file mode 100644
index 00000000..97a66c95
--- /dev/null
+++ b/test-suite/complexity/evar_instance.v
@@ -0,0 +1,78 @@
+(* Checks behavior of unification with respect to the size of evar instances *)
+(* Expected time < 2.00s *)
+
+(* Note that the exact example chosen is not important as soon as it
+   involves a few of each part of the unification algorithme (and especially
+   evar-evar unification and evar-term instantiation) *)
+
+(* In 8.2, the example was in O(n^3) in the number of section variables; 
+   From current commit it is in O(n^2) *)
+
+(* For the record: with coqtop.byte on a Dual Core 2:
+
+   Nb of extra           T  i  m  e
+    variables     8.1    8.2    8.3beta   current
+       800       1.6s   188s    185s      1.6s
+       400       0.5s    24s     24s      0.43s
+       200       0.17s    3s      3.2s    0.12s
+       100       0.06s    0.5s    0.48s   0.04s
+        50       0.02s    0.08s   0.08s   0.016s
+         n      12*a*n^2  a*n^3   a*n^3   8*a*n^2
+*)
+
+Set Implicit Arguments.
+Parameter t:Set->Set.
+Parameter map:forall elt elt' : Set, (elt -> elt') -> t elt -> t elt'.
+Parameter avl: forall elt : Set, t elt -> Prop.
+Parameter bst: forall elt : Set, t elt -> Prop.
+Parameter map_avl: forall (elt elt' : Set) (f : elt -> elt') (m : t elt),
+   avl m -> avl (map f m).
+Parameter map_bst: forall (elt elt' : Set) (f : elt -> elt') (m : t elt),
+   bst m -> bst (map f m).
+Record bbst (elt:Set) : Set :=
+  Bbst {this :> t elt; is_bst : bst this; is_avl: avl this}.
+Definition t' := bbst.
+Section B.
+
+Variables
+ a b c d e f g h i j k m n o p q r s u v w x y z
+ a0 b0 c0 d0 e0 f0 g0 h0 i0 j0 k0 m0 n0 o0 p0 q0 r0 s0 u0 v0 w0 x0 y0 z0
+ a1 b1 c1 d1 e1 f1 g1 h1 i1 j1 k1 m1 n1 o1 p1 q1 r1 s1 u1 v1 w1 x1 y1 z1
+ a2 b2 c2 d2 e2 f2 g2 h2 i2 j2 k2 m2 n2 o2 p2 q2 r2 s2 u2 v2 w2 x2 y2 z2
+ a3 b3 c3 d3 e3 f3 g3 h3 i3 j3 k3 m3 n3 o3 p3 q3 r3 s3 u3 v3 w3 x3 y3 z3
+ a4 b4 c4 d4 e4 f4 g4 h4 i4 j4 k4 m4 n4 o4 p4 q4 r4 s4 u4 v4 w4 x4 y4 z4
+ a5 b5 c5 d5 e5 f5 g5 h5 i5 j5 k5 m5 n5 o5 p5 q5 r5 s5 u5 v5 w5 x5 y5 z5
+ a6 b6 c6 d6 e6 f6 g6 h6 i6 j6 k6 m6 n6 o6 p6 q6 r6 s6 u6 v6 w6 x6 y6 z6
+
+ a7 b7 c7 d7 e7 f7 g7 h7 i7 j7 k7 m7 n7 o7 p7 q7 r7 s7 u7 v7 w7 x7 y7 z7
+ a8 b8 c8 d8 e8 f8 g8 h8 i8 j8 k8 m8 n8 o8 p8 q8 r8 s8 u8 v8 w8 x8 y8 z8
+ a9 b9 c9 d9 e9 f9 g9 h9 i9 j9 k9 m9 n9 o9 p9 q9 r9 s9 u9 v9 w9 x9 y9 z9
+ aA bA cA dA eA fA gA hA iA jA kA mA nA oA pA qA rA sA uA vA wA xA yA zA
+ aB bB cB dB eB fB gB hB iB jB kB mB nB oB pB qB rB sB uB vB wB xB yB zB
+ aC bC cC dC eC fC gC hC iC jC kC mC nC oC pC qC rC sC uC vC wC xC yC zC
+ aD bD cD dD eD fD gD hD iD jD kD mD nD oD pD qD rD sD uD vD wD xD yD zD
+ aE bE cE dE eE fE gE hE iE jE kE mE nE oE pE qE rE sE uE vE wE xE yE zE
+
+ aF bF cF dF eF fF gF hF iF jF kF mF nF oF pF qF rF sF uF vF wF xF yF zF
+ aG bG cG dG eG fG gG hG iG jG kG mG nG oG pG qG rG sG uG vG wG xG yG zG
+ aH bH cH dH eH fH gH hH iH jH kH mH nH oH pH qH rH sH uH vH wH xH yH zH
+ aI bI cI dI eI fI gI hI iI jI kI mI nI oI pI qI rI sI uI vI wI xI yI zI
+ aJ bJ cJ dJ eJ fJ gJ hJ iJ jJ kJ mJ nJ oJ pJ qJ rJ sJ uJ vJ wJ xJ yJ zJ
+ aK bK cK dK eK fK gK hK iK jK kK mK nK oK pK qK rK sK uK vK wK xK yK zK
+ aL bL cL dL eL fL gL hL iL jL kL mL nL oL pL qL rL sL uL vL wL xL yL zL
+ aM bM cM dM eM fM gM hM iM jM kM mM nM oM pM qM rM sM uM vM wM xM yM zM
+
+ aN bN cN dN eN fN gN hN iN jN kN mN nN oN pN qN rN sN uN vN wN xN yN zN
+ aO bO cO dO eO fO gO hO iO jO kO mO nO oO pO qO rO sO uO vO wO xO yO zO
+ aP bP cP dP eP fP gP hP iP jP kP mP nP oP pP qP rP sP uP vP wP xP yP zP
+ aQ bQ cQ dQ eQ fQ gQ hQ iQ jQ kQ mQ nQ oQ pQ qQ rQ sQ uQ vQ wQ xQ yQ zQ
+ aR bR cR dR eR fR gR hR iR jR kR mR nR oR pR qR rR sR uR vR wR xR yR zR
+ aS bS cS dS eS fS gS hS iS jS kS mS nS oS pS qS rS sS uS vS wS xS yS zS
+ aT bT cT dT eT fT gT hT iT jT kT mT nT oT pT qT rT sT uT vT wT xT yT zT
+ aU bU cU dU eU fU gU hU iU jU kU mU nU oU pU qU rU sU uU vU wU xU yU zU
+
+ : nat .
+
+Variables elt elt': Set.
+Timeout 5 Time Definition map' f (m:t' elt) : t' elt' :=
+  Bbst (map_bst f m.(is_bst)) (map_avl f m.(is_avl)).
diff --git a/test-suite/complexity/guard.v b/test-suite/complexity/guard.v
new file mode 100644
index 00000000..ceb7835a
--- /dev/null
+++ b/test-suite/complexity/guard.v
@@ -0,0 +1,30 @@
+(* Examples to check that the guard condition does not evaluate
+   irrelevant subterms *)
+(* Expected time < 1.00s *)
+Require Import Bool.
+
+Fixpoint slow n :=
+ match n with
+ | 0 => true
+ | S k => andb (slow k) (slow k)
+ end.
+
+Timeout 5 Time Fixpoint F n :=
+  match n with
+  | 0 => 0
+  | S k =>
+    if slow 100 then F k else 0
+  end.
+
+Fixpoint slow2 n :=
+ match n with
+ | 0 => 0
+ | S k => slow2 k + slow2 k
+ end.
+
+Timeout 5 Time Fixpoint F' n :=
+  match n with
+  | 0 => 0
+  | S k =>
+    if slow2 100 then F' k else 0
+  end.
diff --git a/test-suite/complexity/patternmatching.v b/test-suite/complexity/patternmatching.v
new file mode 100644
index 00000000..7b628136
--- /dev/null
+++ b/test-suite/complexity/patternmatching.v
@@ -0,0 +1,8 @@
+(* This example checks the efficiency of pattern-matching compilation on simple cases *)
+(* Expected time < 1.00s *)
+
+Time Definition a400 n := match n with
+  S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S x))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) => x
+| _ => 0
+end.
+
diff --git a/test-suite/complexity/ring2.v b/test-suite/complexity/ring2.v
index ab57afdb..6945edc8 100644
--- a/test-suite/complexity/ring2.v
+++ b/test-suite/complexity/ring2.v
@@ -11,7 +11,7 @@ match x with
     | 0%Z => x
     | Zpos y' => Zpos (x' + y')
     | Zneg y' =>
-        match (x' ?= y')%positive Eq with
+        match (x' ?= y')%positive with
         | Eq => 0%Z
         | Lt => Zneg (y' - x')
         | Gt => Zpos (x' - y')
@@ -21,7 +21,7 @@ match x with
     match y with
     | 0%Z => x
     | Zpos y' =>
-        match (x' ?= y')%positive Eq with
+        match (x' ?= y')%positive with
         | Eq => 0%Z
         | Lt => Zpos (y' - x')
         | Gt => Zneg (x' - y')
diff --git a/test-suite/csdp.cache b/test-suite/csdp.cache
index 645de69c..297ac255 100644
--- a/test-suite/csdp.cache
+++ b/test-suite/csdp.cache
diff --git a/test-suite/failure/Tauto.v b/test-suite/failure/Tauto.v
index 96e66a0d..a08c5154 100644
--- a/test-suite/failure/Tauto.v
+++ b/test-suite/failure/Tauto.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/test-suite/failure/clash_cons.v b/test-suite/failure/clash_cons.v
index 3f8d8784..d000f965 100644
--- a/test-suite/failure/clash_cons.v
+++ b/test-suite/failure/clash_cons.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/test-suite/failure/fixpoint1.v b/test-suite/failure/fixpoint1.v
index e4ef6c95..e38fa6e0 100644
--- a/test-suite/failure/fixpoint1.v
+++ b/test-suite/failure/fixpoint1.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/test-suite/failure/guard.v b/test-suite/failure/guard.v
index e5915ab1..079ad33f 100644
--- a/test-suite/failure/guard.v
+++ b/test-suite/failure/guard.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/test-suite/failure/illtype1.v b/test-suite/failure/illtype1.v
index ed48c6c2..64537877 100644
--- a/test-suite/failure/illtype1.v
+++ b/test-suite/failure/illtype1.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/test-suite/failure/inductive4.v b/test-suite/failure/inductive4.v
new file mode 100644
index 00000000..6ba36fd2
--- /dev/null
+++ b/test-suite/failure/inductive4.v
@@ -0,0 +1,15 @@
+(* This used to succeed in versions 8.1 to 8.3 *)
+
+Require Import Logic.
+Require Hurkens.
+Definition Ti := Type.
+Inductive prod (X Y:Ti) := pair : X -> Y -> prod X Y.
+Definition B : Prop := let F := prod True in F Prop. (* Aie! *)
+Definition p2b (P:Prop) : B := pair True Prop I P.
+Definition b2p (b:B) : Prop := match b with pair _ P => P end.
+Lemma L1 : forall A : Prop, b2p (p2b A) -> A.
+Proof (fun A x => x).
+Lemma L2 : forall A : Prop, A -> b2p (p2b A).
+Proof (fun A x => x).
+Check Hurkens.paradox B p2b b2p L1 L2.
+
diff --git a/test-suite/failure/positivity.v b/test-suite/failure/positivity.v
index c02661e0..e9fbe969 100644
--- a/test-suite/failure/positivity.v
+++ b/test-suite/failure/positivity.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/test-suite/failure/redef.v b/test-suite/failure/redef.v
index 71d49b58..2b648c13 100644
--- a/test-suite/failure/redef.v
+++ b/test-suite/failure/redef.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/test-suite/failure/search.v b/test-suite/failure/search.v
index ebbd5ca0..0ff554d9 100644
--- a/test-suite/failure/search.v
+++ b/test-suite/failure/search.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/test-suite/failure/universes2.v b/test-suite/failure/universes2.v
deleted file mode 100644
index e74de70f..00000000
--- a/test-suite/failure/universes2.v
+++ /dev/null
@@ -1,4 +0,0 @@
-(* Example submitted by Randy Pollack *)
-
-Parameter K : forall T : Type, T -> T.
-Check (K (forall T : Type, T -> T) K).
diff --git a/test-suite/ide/undo.v b/test-suite/ide/undo.v
index d5e9ee5e..ea392055 100644
--- a/test-suite/ide/undo.v
+++ b/test-suite/ide/undo.v
@@ -3,8 +3,8 @@
 
 (* Undoing arbitrary commands, as first step *)
 
-Theorem a : O=O.
-Ltac f x := x.
+Theorem a : O=O. (* 2 *)
+Ltac f x := x. (* 1 * 3 *)
 assert True by trivial.
 trivial.
 Qed.
@@ -79,6 +79,7 @@ Definition q := O.
 Definition r := O.
 
 (* Bug 2082 : Follow the numbers *)
+(* Broken due to proof engine rewriting *)
 
 Variable A : Prop.
 Variable B : Prop.
diff --git a/test-suite/ide/undo001.fake b/test-suite/ide/undo001.fake
new file mode 100644
index 00000000..bbaea7e7
--- /dev/null
+++ b/test-suite/ide/undo001.fake
@@ -0,0 +1,10 @@
+# Script simulating a dialog between coqide and coqtop -ideslave
+# Run it via fake_ide
+#
+# Simple backtrack by 1 between two global definitions
+#
+INTERP Definition foo := 0.
+INTERP Definition bar := 1.
+REWIND 1
+INTERPRAW Check foo.
+INTERPRAW Fail Check bar.
diff --git a/test-suite/ide/undo002.fake b/test-suite/ide/undo002.fake
new file mode 100644
index 00000000..b855b6ea
--- /dev/null
+++ b/test-suite/ide/undo002.fake
@@ -0,0 +1,10 @@
+# Script simulating a dialog between coqide and coqtop -ideslave
+# Run it via fake_ide
+#
+# Simple backtrack by 2 before two global definitions
+#
+INTERP Definition foo := 0.
+INTERP Definition bar := 1.
+REWIND 2
+INTERPRAW Fail Check foo.
+INTERPRAW Fail Check bar.
diff --git a/test-suite/ide/undo003.fake b/test-suite/ide/undo003.fake
new file mode 100644
index 00000000..4c72e8dc
--- /dev/null
+++ b/test-suite/ide/undo003.fake
@@ -0,0 +1,8 @@
+# Script simulating a dialog between coqide and coqtop -ideslave
+# Run it via fake_ide
+#
+# Simple backtrack by 0 should be a no-op
+#
+INTERP Definition foo := 0.
+REWIND 0
+INTERPRAW Check foo.
diff --git a/test-suite/ide/undo004.fake b/test-suite/ide/undo004.fake
new file mode 100644
index 00000000..c2ddfb8c
--- /dev/null
+++ b/test-suite/ide/undo004.fake
@@ -0,0 +1,14 @@
+# Script simulating a dialog between coqide and coqtop -ideslave
+# Run it via fake_ide
+#
+# Undoing arbitrary commands, as first step
+#
+INTERP Theorem a : O=O.
+INTERP Ltac f x := x.
+REWIND 1
+# <replay>
+INTERP Ltac f x := x.
+# <\replay>
+INTERP assert True by trivial.
+INTERP trivial.
+INTERP Qed.
diff --git a/test-suite/ide/undo005.fake b/test-suite/ide/undo005.fake
new file mode 100644
index 00000000..525b9f2a
--- /dev/null
+++ b/test-suite/ide/undo005.fake
@@ -0,0 +1,15 @@
+# Script simulating a dialog between coqide and coqtop -ideslave
+# Run it via fake_ide
+#
+# Undoing arbitrary commands, as non-first step
+#
+INTERP Theorem b : O=O.
+INTERP assert True by trivial.
+INTERP Ltac g x := x.
+# <replay>
+REWIND 1
+# <\replay>
+INTERP Ltac g x := x.
+INTERP assert True by trivial.
+INTERP trivial.
+INTERP Qed.
diff --git a/test-suite/ide/undo006.fake b/test-suite/ide/undo006.fake
new file mode 100644
index 00000000..ed88bef5
--- /dev/null
+++ b/test-suite/ide/undo006.fake
@@ -0,0 +1,14 @@
+# Script simulating a dialog between coqide and coqtop -ideslave
+# Run it via fake_ide
+#
+# Undoing declarations, as first step
+# Was bugged in 8.1
+#
+INTERP Theorem c : O=O.
+INTERP Inductive T : Type := I.
+REWIND 1
+# <replay>
+INTERP Inductive T : Type := I.
+# <\replay>
+INTERP trivial.
+INTERP Qed.
diff --git a/test-suite/ide/undo007.fake b/test-suite/ide/undo007.fake
new file mode 100644
index 00000000..87c06dbb
--- /dev/null
+++ b/test-suite/ide/undo007.fake
@@ -0,0 +1,17 @@
+# Script simulating a dialog between coqide and coqtop -ideslave
+# Run it via fake_ide
+#
+# Undoing declarations, as first step
+# new in 8.2
+#
+INTERP Theorem d : O=O.
+INTERP Definition e := O.
+INTERP Definition f := O.
+REWIND 1
+# <replay>
+INTERP Definition f := O.
+# <\replay>
+INTERP assert True by trivial.
+INTERP trivial.
+INTERP Qed.
+INTERPRAW Check e.
diff --git a/test-suite/ide/undo008.fake b/test-suite/ide/undo008.fake
new file mode 100644
index 00000000..1c46c1e8
--- /dev/null
+++ b/test-suite/ide/undo008.fake
@@ -0,0 +1,18 @@
+# Script simulating a dialog between coqide and coqtop -ideslave
+# Run it via fake_ide
+#
+# Undoing declarations, as non-first step
+# new in 8.2
+#
+INTERP Theorem h : O=O.
+INTERP assert True by trivial.
+INTERP Definition i := O.
+INTERP Definition j := O.
+REWIND 1
+# <replay>
+INTERP Definition j := O.
+# <\replay>
+INTERP assert True by trivial.
+INTERP trivial.
+INTERP Qed.
+INTERPRAW Check i.
diff --git a/test-suite/ide/undo009.fake b/test-suite/ide/undo009.fake
new file mode 100644
index 00000000..47c77d23
--- /dev/null
+++ b/test-suite/ide/undo009.fake
@@ -0,0 +1,20 @@
+# Script simulating a dialog between coqide and coqtop -ideslave
+# Run it via fake_ide
+#
+# Undoing declarations, interleaved with proof steps
+# new in 8.2 *)
+#
+INTERP Theorem k : O=O.
+INTERP assert True by trivial.
+INTERP Definition l := O.
+INTERP assert True by trivial.
+INTERP Definition m := O.
+REWIND 3
+# <replay>
+INTERP Definition l := O.
+INTERP assert True by trivial.
+INTERP Definition m := O.
+# <\replay>
+INTERP assert True by trivial.
+INTERP trivial.
+INTERP Qed.
diff --git a/test-suite/ide/undo010.fake b/test-suite/ide/undo010.fake
new file mode 100644
index 00000000..4fe9df98
--- /dev/null
+++ b/test-suite/ide/undo010.fake
@@ -0,0 +1,28 @@
+# Script simulating a dialog between coqide and coqtop -ideslave
+# Run it via fake_ide
+#
+# Undoing declarations, interleaved with proof steps and commands *)
+# new in 8.2 *)
+#
+INTERP Theorem n : O=O.
+INTERP assert True by trivial.
+INTERP Definition o := O.
+INTERP Ltac h x := x.
+INTERP assert True by trivial.
+INTERP Focus.
+INTERP Definition p := O.
+REWIND 1
+REWIND 1
+REWIND 1
+REWIND 1
+REWIND 1
+# <replay>
+INTERP Definition o := O.
+INTERP Ltac h x := x.
+INTERP assert True by trivial.
+INTERP Focus.
+INTERP Definition p := O.
+# </replay>
+INTERP assert True by trivial.
+INTERP trivial.
+INTERP Qed.
diff --git a/test-suite/ide/undo011.fake b/test-suite/ide/undo011.fake
new file mode 100644
index 00000000..cc85a764
--- /dev/null
+++ b/test-suite/ide/undo011.fake
@@ -0,0 +1,32 @@
+# Script simulating a dialog between coqide and coqtop -ideslave
+# Run it via fake_ide
+#
+# Bug 2082
+# Broken due to proof engine rewriting
+#
+INTERP Variable A : Prop.
+INTERP Variable B : Prop.
+INTERP Axiom OR : A \/ B.
+INTERP Lemma MyLemma2 : True.
+INTERP proof.
+INTERP per cases of (A \/ B) by OR.
+INTERP suppose A.
+INTERP     then (1 = 1).
+INTERP     then H1 : thesis.
+INTERP     thus thesis by H1.
+INTERP suppose B.
+REWIND 1
+# <replay>
+INTERP suppose B.
+# </replay>
+REWIND 2
+# <replay>
+INTERP     thus thesis by H1.
+INTERP suppose B.
+# </replay>
+INTERP    then (1 = 1).
+INTERP    then H2 : thesis.
+INTERP    thus thesis by H2.
+INTERP end cases.
+INTERP end proof.
+INTERP Qed.
diff --git a/test-suite/ide/undo012.fake b/test-suite/ide/undo012.fake
new file mode 100644
index 00000000..f9b29ca1
--- /dev/null
+++ b/test-suite/ide/undo012.fake
@@ -0,0 +1,26 @@
+# Script simulating a dialog between coqide and coqtop -ideslave
+# Run it via fake_ide
+#
+# Test backtracking in presence of nested proofs
+# First, undoing the whole
+#
+INTERP Lemma aa : True -> True /\ True.
+INTERP intro H.
+INTERP split.
+INTERP Lemma bb : False -> False.
+INTERP intro H.
+INTERP apply H.
+INTERP Qed.
+INTERP apply H.
+INTERP Lemma cc : False -> True.
+INTERP intro H.
+INTERP destruct H.
+INTERP Qed.
+INTERP apply H.
+INTERP Qed.
+REWIND 1
+# We should now be just before aa, without opened proofs
+INTERPRAW Fail idtac.
+INTERPRAW Fail Check aa.
+INTERPRAW Fail Check bb.
+INTERPRAW Fail Check cc.
diff --git a/test-suite/ide/undo013.fake b/test-suite/ide/undo013.fake
new file mode 100644
index 00000000..3b1c61e6
--- /dev/null
+++ b/test-suite/ide/undo013.fake
@@ -0,0 +1,31 @@
+# Script simulating a dialog between coqide and coqtop -ideslave
+# Run it via fake_ide
+#
+# Test backtracking in presence of nested proofs
+# Second, trigger the full undo of an inner proof
+#
+INTERP Lemma aa : True -> True /\ True.
+INTERP intro H.
+INTERP split.
+INTERP Lemma bb : False -> False.
+INTERP intro H.
+INTERP apply H.
+INTERP Qed.
+INTERP apply H.
+INTERP Lemma cc : False -> True.
+INTERP intro H.
+INTERP destruct H.
+INTERP Qed.
+INTERP apply H.
+REWIND 2
+# We should now be just before "Lemma cc"
+# <replay>
+INTERP Lemma cc : False -> True.
+INTERP intro H.
+INTERP destruct H.
+INTERP Qed.
+INTERP apply H.
+# </replay>
+INTERP Qed.
+INTERPRAW Fail idtac.
+INTERPRAW Check (aa,bb,cc).
diff --git a/test-suite/ide/undo014.fake b/test-suite/ide/undo014.fake
new file mode 100644
index 00000000..5224b504
--- /dev/null
+++ b/test-suite/ide/undo014.fake
@@ -0,0 +1,26 @@
+# Script simulating a dialog between coqide and coqtop -ideslave
+# Run it via fake_ide
+#
+# Test backtracking in presence of nested proofs
+# Third, undo inside an inner proof
+#
+INTERP Lemma aa : True -> True /\ True.
+INTERP intro H.
+INTERP split.
+INTERP Lemma bb : False -> False.
+INTERP intro H.
+INTERP apply H.
+INTERP Qed.
+INTERP apply H.
+INTERP Lemma cc : False -> True.
+INTERP intro H.
+INTERP destruct H.
+REWIND 1
+# <replay>
+INTERP destruct H.
+# </replay>
+INTERP Qed.
+INTERP apply H.
+INTERP Qed.
+INTERPRAW Fail idtac.
+INTERPRAW Check (aa,bb,cc).
diff --git a/test-suite/ide/undo015.fake b/test-suite/ide/undo015.fake
new file mode 100644
index 00000000..32e46ec9
--- /dev/null
+++ b/test-suite/ide/undo015.fake
@@ -0,0 +1,29 @@
+# Script simulating a dialog between coqide and coqtop -ideslave
+# Run it via fake_ide
+#
+# Test backtracking in presence of nested proofs
+# Fourth, undo from an inner proof to a above proof
+#
+INTERP Lemma aa : True -> True /\ True.
+INTERP intro H.
+INTERP split.
+INTERP Lemma bb : False -> False.
+INTERP intro H.
+INTERP apply H.
+INTERP Qed.
+INTERP apply H.
+INTERP Lemma cc : False -> True.
+INTERP intro H.
+INTERP destruct H.
+REWIND 4
+# <replay>
+INTERP apply H.
+INTERP Lemma cc : False -> True.
+INTERP intro H.
+INTERP destruct H.
+# </replay>
+INTERP Qed.
+INTERP apply H.
+INTERP Qed.
+INTERPRAW Fail idtac.
+INTERPRAW Check (aa,bb,cc).
diff --git a/test-suite/ide/undo016.fake b/test-suite/ide/undo016.fake
new file mode 100644
index 00000000..2a6e512c
--- /dev/null
+++ b/test-suite/ide/undo016.fake
@@ -0,0 +1,34 @@
+# Script simulating a dialog between coqide and coqtop -ideslave
+# Run it via fake_ide
+#
+# Test backtracking in presence of nested proofs
+# Fifth, undo from an inner proof to a previous inner proof
+#
+INTERP Lemma aa : True -> True /\ True.
+INTERP intro H.
+INTERP split.
+INTERP Lemma bb : False -> False.
+INTERP intro H.
+INTERP apply H.
+INTERP Qed.
+INTERP apply H.
+INTERP Lemma cc : False -> True.
+INTERP intro H.
+INTERP destruct H.
+REWIND 6
+# We should be just before "Lemma bb"
+# <replay>
+INTERP Lemma bb : False -> False.
+INTERP intro H.
+INTERP apply H.
+INTERP Qed.
+INTERP apply H.
+INTERP Lemma cc : False -> True.
+INTERP intro H.
+INTERP destruct H.
+# </replay>
+INTERP Qed.
+INTERP apply H.
+INTERP Qed.
+INTERPRAW Fail idtac.
+INTERPRAW Check (aa,bb,cc).
diff --git a/test-suite/ide/undo017.fake b/test-suite/ide/undo017.fake
new file mode 100644
index 00000000..232360e9
--- /dev/null
+++ b/test-suite/ide/undo017.fake
@@ -0,0 +1,13 @@
+# Script simulating a dialog between coqide and coqtop -ideslave
+# Run it via fake_ide
+#
+# bug #2569 : Undoing inside modules
+#
+INTERP Module M.
+INTERP Definition x := 0.
+INTERP End M.
+REWIND 1
+# <replay>
+INTERP End M.
+# </replay>
+INTERPRAW Check M.x.
diff --git a/test-suite/ide/undo018.fake b/test-suite/ide/undo018.fake
new file mode 100644
index 00000000..ef0945ab
--- /dev/null
+++ b/test-suite/ide/undo018.fake
@@ -0,0 +1,13 @@
+# Script simulating a dialog between coqide and coqtop -ideslave
+# Run it via fake_ide
+#
+# bug #2569 : Undoing inside section
+#
+INTERP Section M.
+INTERP Definition x := 0.
+INTERP End M.
+REWIND 1
+# <replay>
+INTERP End M.
+# </replay>
+INTERPRAW Check x.
diff --git a/test-suite/ide/undo019.fake b/test-suite/ide/undo019.fake
new file mode 100644
index 00000000..70e70d7e
--- /dev/null
+++ b/test-suite/ide/undo019.fake
@@ -0,0 +1,14 @@
+# Script simulating a dialog between coqide and coqtop -ideslave
+# Run it via fake_ide
+#
+# bug #2569 : Undoing a focused subproof
+#
+INTERP Goal True.
+INTERP {
+INTERP exact I.
+INTERP }
+REWIND 1
+# <replay>
+INTERP }
+# </replay>
+INTERP Qed.
diff --git a/test-suite/ideal-features/Apply.v b/test-suite/ideal-features/Apply.v
index db52af2f..8b36f44b 100644
--- a/test-suite/ideal-features/Apply.v
+++ b/test-suite/ideal-features/Apply.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/test-suite/ideal-features/Case8.v b/test-suite/ideal-features/Case8.v
deleted file mode 100644
index 2ac5bd8c..00000000
--- a/test-suite/ideal-features/Case8.v
+++ /dev/null
@@ -1,36 +0,0 @@
-Inductive listn : nat -> Set :=
-  | niln : listn 0
-  | consn : forall n : nat, nat -> listn n -> listn (S n).
-
-Inductive empty : forall n : nat, listn n -> Prop :=
-    intro_empty : empty 0 niln.
-
-Parameter
-  inv_empty : forall (n a : nat) (l : listn n), ~ empty (S n) (consn n a l).
-
-Type
-  (fun (n : nat) (l : listn n) =>
-   match l in (listn n) return (empty n l \/ ~ empty n l) with
-   | niln => or_introl (~ empty 0 niln) intro_empty
-   | consn n O y as b => or_intror (empty (S n) b) (inv_empty n 0 y)
-   | consn n a y as b => or_intror (empty (S n) b) (inv_empty n a y)
-   end).
-
-
-Type
-  (fun (n : nat) (l : listn n) =>
-   match l in (listn n) return (empty n l \/ ~ empty n l) with
-   | niln => or_introl (~ empty 0 niln) intro_empty
-   | consn n O y => or_intror (empty (S n) (consn n 0 y)) (inv_empty n 0 y)
-   | consn n a y => or_intror (empty (S n) (consn n a y)) (inv_empty n a y)
-   end).
-
-
-
-Type
-  (fun (n : nat) (l : listn n) =>
-   match l in (listn n) return (empty n l \/ ~ empty n l) with
-   | niln => or_introl (~ empty 0 niln) intro_empty
-   | consn O a y as b => or_intror (empty 1 b) (inv_empty 0 a y)
-   | consn n a y as b => or_intror (empty (S n) b) (inv_empty n a y)
-   end).
diff --git a/test-suite/micromega/csdp.cache b/test-suite/micromega/csdp.cache
deleted file mode 100644
index 645de69c..00000000
--- a/test-suite/micromega/csdp.cache
+++ /dev/null
diff --git a/test-suite/misc/berardi_test.v b/test-suite/misc/berardi_test.v
index da54166a..2b388687 100644
--- a/test-suite/misc/berardi_test.v
+++ b/test-suite/misc/berardi_test.v
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 (** This file formalizes Berardi's paradox which says that in
    the calculus of constructions, excluded middle (EM) and axiom of
    choice (AC) imply proof irrelevance (PI).
diff --git a/test-suite/misc/deps/deps.out b/test-suite/misc/deps/deps.out
index 68b48d60..5b79349f 100644
--- a/test-suite/misc/deps/deps.out
+++ b/test-suite/misc/deps/deps.out
@@ -1 +1 @@
-misc/deps/client/bar.vo misc/deps/client/bar.glob: misc/deps/client/bar.v misc/deps/client/foo.vo misc/deps/lib/foo.vo
+misc/deps/client/bar.vo misc/deps/client/bar.glob misc/deps/client/bar.v.beautified: misc/deps/client/bar.v misc/deps/client/foo.vo misc/deps/lib/foo.vo
diff --git a/test-suite/misc/universes/universes.v b/test-suite/misc/universes/universes.v
new file mode 100644
index 00000000..b7c7ed81
--- /dev/null
+++ b/test-suite/misc/universes/universes.v
@@ -0,0 +1,2 @@
+Require all_stdlib.
+Print Sorted Universes "universes.txt".
diff --git a/test-suite/modules/errors.v b/test-suite/modules/errors.v
new file mode 100644
index 00000000..d1658786
--- /dev/null
+++ b/test-suite/modules/errors.v
@@ -0,0 +1,70 @@
+(* Inductive mismatches *)
+
+Module Type SA. Inductive TA : nat -> Prop := CA : nat -> TA 0. End SA.
+Module MA : SA. Inductive TA : Prop := CA : bool -> TA. Fail End MA.
+
+Module Type SA. Inductive TA := CA : nat -> TA. End SA.
+Module MA : SA. Inductive TA := CA : bool -> TA. Fail End MA.
+
+Module Type SA. Inductive TA := CA : nat -> TA. End SA.
+Module MA : SA. Inductive TA := CA : bool -> nat -> TA. Fail End MA.
+
+Module Type SA2. Inductive TA2 := CA2 : nat -> TA2. End SA2.
+Module MA2 : SA2. Inductive TA2 := CA2 : nat -> TA2 | DA2 : TA2. Fail End MA2.
+
+Module Type SA3. Inductive TA3 := CA3 : nat -> TA3. End SA3.
+Module MA3 : SA3. Inductive TA3 := CA3 : nat -> TA3 with UA3 := DA3. Fail End MA3.
+
+Module Type SA4. Inductive TA4 := CA4 : nat -> TA4 with UA4 := DA4. End SA4.
+Module MA4 : SA4. Inductive TA4 := CA4 : nat -> TA4 with VA4 := DA4. Fail End MA4.
+
+Module Type SA5. Inductive TA5 := CA5 : nat -> TA5 with UA5 := DA5. End SA5.
+Module MA5 : SA5. Inductive TA5 := CA5 : nat -> TA5 with UA5 := EA5. Fail End MA5.
+
+Module Type SA6. Inductive TA6 (A:Type) := CA6 : A -> TA6 A. End SA6.
+Module MA6 : SA6. Inductive TA6 (A B:Type):= CA6 : A -> TA6 A B. Fail End MA6.
+
+Module Type SA7. Inductive TA7 (A:Type) := CA7 : A -> TA7 A. End SA7.
+Module MA7 : SA7. CoInductive TA7 (A:Type):= CA7 : A -> TA7 A. Fail End MA7.
+
+Module Type SA8. CoInductive TA8 (A:Type) := CA8 : A -> TA8 A. End SA8.
+Module MA8 : SA8. Inductive TA8 (A:Type):= CA8 : A -> TA8 A. Fail End MA8.
+
+Module Type SA9. Record TA9 (A:Type) := { CA9 : A }. End SA9.
+Module MA9 : SA9. Inductive TA9 (A:Type):= CA9 : A -> TA9 A. Fail End MA9.
+
+Module Type SA10. Inductive TA10 (A:Type) := CA10 : A -> TA10 A. End SA10.
+Module MA10 : SA10. Record TA10 (A:Type):= { CA10 : A }. Fail End MA10.
+
+Module Type SA11. Record TA11 (A:Type):= { CA11 : A }. End SA11.
+Module MA11 : SA11. Record TA11 (A:Type):= { DA11 : A }. Fail End MA11.
+
+(* Basic mismatches *)
+Module Type SB. Inductive TB := CB : nat -> TB. End SB.
+Module MB : SB. Module Type TB. End TB. Fail End MB.
+
+Module Type SC. Module Type TC. End TC. End SC.
+Module MC : SC. Inductive TC := CC : nat -> TC. Fail End MC.
+
+Module Type SD. Module TD. End TD. End SD.
+Module MD : SD. Inductive TD := DD : nat -> TD. Fail End MD.
+
+Module Type SE. Definition DE := nat. End SE.
+Module ME : SE. Definition DE := bool. Fail End ME.
+
+Module Type SF. Parameter DF : nat. End SF.
+Module MF : SF. Definition DF := bool. Fail End MF.
+
+(* Needs a type constraint in module type *)
+Module Type SG. Definition DG := Type. End SG.
+Module MG : SG. Definition DG := Type : Type. Fail End MG.
+
+(* Should work *)
+Module Type SA7. Inductive TA7 (A:Type) := CA7 : A -> TA7 A. End SA7.
+Module MA7 : SA7. Inductive TA7 (B:Type):= CA7 : B -> TA7 B. End MA7.
+
+Module Type SA11. Record TA11 (B:Type):= { CA11 : B }. End SA11.
+Module MA11 : SA11. Record TA11 (A:Type):= { CA11 : A }. End MA11.
+
+Module Type SE. Parameter DE : Type. End SE.
+Module ME : SE. Definition DE := Type : Type. End ME.
diff --git a/test-suite/output/Arguments.out b/test-suite/output/Arguments.out
new file mode 100644
index 00000000..139f9e99
--- /dev/null
+++ b/test-suite/output/Arguments.out
@@ -0,0 +1,93 @@
+minus : nat -> nat -> nat
+
+Argument scopes are [nat_scope nat_scope]
+The simpl tactic unfolds minus avoiding to expose match constructs
+minus is transparent
+Expands to: Constant Coq.Init.Peano.minus
+minus : nat -> nat -> nat
+
+Argument scopes are [nat_scope nat_scope]
+The simpl tactic unfolds minus when applied to 1 argument
+  avoiding to expose match constructs
+minus is transparent
+Expands to: Constant Coq.Init.Peano.minus
+minus : nat -> nat -> nat
+
+Argument scopes are [nat_scope nat_scope]
+The simpl tactic unfolds minus
+  when the 1st argument evaluates to a constructor and
+  when applied to 1 argument avoiding to expose match constructs
+minus is transparent
+Expands to: Constant Coq.Init.Peano.minus
+minus : nat -> nat -> nat
+
+Argument scopes are [nat_scope nat_scope]
+The simpl tactic unfolds minus
+  when the 1st and 2nd arguments evaluate to a constructor and
+  when applied to 2 arguments 
+minus is transparent
+Expands to: Constant Coq.Init.Peano.minus
+minus : nat -> nat -> nat
+
+Argument scopes are [nat_scope nat_scope]
+The simpl tactic unfolds minus
+  when the 1st and 2nd arguments evaluate to a constructor 
+minus is transparent
+Expands to: Constant Coq.Init.Peano.minus
+pf :
+forall D1 C1 : Type,
+(D1 -> C1) -> forall D2 C2 : Type, (D2 -> C2) -> D1 * D2 -> C1 * C2
+
+Arguments D2, C2 are implicit
+Arguments D1, C1 are implicit and maximally inserted
+Argument scopes are [foo_scope type_scope _ _ _ _ _]
+The simpl tactic never unfolds pf
+pf is transparent
+Expands to: Constant Top.pf
+fcomp : forall A B C : Type, (B -> C) -> (A -> B) -> A -> C
+
+Arguments A, B, C are implicit and maximally inserted
+Argument scopes are [type_scope type_scope type_scope _ _ _]
+The simpl tactic unfolds fcomp when applied to 6 arguments 
+fcomp is transparent
+Expands to: Constant Top.fcomp
+volatile : nat -> nat
+
+Argument scope is [nat_scope]
+The simpl tactic always unfolds volatile
+volatile is transparent
+Expands to: Constant Top.volatile
+f : T1 -> T2 -> nat -> unit -> nat -> nat
+
+Argument scopes are [_ _ nat_scope _ nat_scope]
+f is transparent
+Expands to: Constant Top.S1.S2.f
+f : T1 -> T2 -> nat -> unit -> nat -> nat
+
+Argument scopes are [_ _ nat_scope _ nat_scope]
+The simpl tactic unfolds f
+  when the 3rd, 4th and 5th arguments evaluate to a constructor 
+f is transparent
+Expands to: Constant Top.S1.S2.f
+f : forall T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat
+
+Argument T2 is implicit
+Argument scopes are [type_scope _ _ nat_scope _ nat_scope]
+The simpl tactic unfolds f
+  when the 4th, 5th and 6th arguments evaluate to a constructor 
+f is transparent
+Expands to: Constant Top.S1.f
+f : forall T1 T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat
+
+Arguments T1, T2 are implicit
+Argument scopes are [type_scope type_scope _ _ nat_scope _ nat_scope]
+The simpl tactic unfolds f
+  when the 5th, 6th and 7th arguments evaluate to a constructor 
+f is transparent
+Expands to: Constant Top.f
+f : forall T1 T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat
+
+The simpl tactic unfolds f
+  when the 5th, 6th and 7th arguments evaluate to a constructor 
+f is transparent
+Expands to: Constant Top.f
diff --git a/test-suite/output/Arguments.v b/test-suite/output/Arguments.v
new file mode 100644
index 00000000..3a94f19a
--- /dev/null
+++ b/test-suite/output/Arguments.v
@@ -0,0 +1,40 @@
+Arguments minus n m : simpl nomatch. 
+About minus.
+Arguments minus n / m : simpl nomatch. 
+About minus.
+Arguments minus !n / m : simpl nomatch. 
+About minus.
+Arguments minus !n !m /.
+About minus.
+Arguments minus !n !m.
+About minus.
+Definition pf (D1 C1 : Type) (f : D1 -> C1) (D2 C2 : Type) (g : D2 -> C2) := 
+  fun x => (f (fst x), g (snd x)).
+Delimit Scope foo_scope with F.
+Arguments pf {D1%F C1%type} f [D2 C2] g x : simpl never.
+About pf.
+Definition fcomp A B C f (g : A -> B) (x : A) : C := f (g x).
+Arguments fcomp {_ _ _}%type_scope f g x /.
+About fcomp.
+Definition volatile := fun x : nat => x.
+Arguments volatile /.
+About volatile.
+Set Implicit Arguments.
+Section S1.
+Variable T1 : Type.
+Section S2.
+Variable T2 : Type.
+Fixpoint f (x : T1) (y : T2) n (v : unit) m {struct n} : nat :=
+  match n, m with
+  | 0,_ => 0
+  | S _, 0 => n
+  | S n', S m' => f x y n' v m' end.
+About f.
+Global Arguments f x y !n !v !m.
+About f.
+End S2.
+About f.
+End S1.
+About f.
+Arguments f : clear implicits and scopes.
+About f.
diff --git a/test-suite/output/ArgumentsScope.out b/test-suite/output/ArgumentsScope.out
index 6643c142..756e8ede 100644
--- a/test-suite/output/ArgumentsScope.out
+++ b/test-suite/output/ArgumentsScope.out
@@ -21,6 +21,11 @@ negb : bool -> bool
 Argument scope is [bool_scope]
 negb is transparent
 Expands to: Constant Coq.Init.Datatypes.negb
+Warning: Arguments Scope is deprecated; use Arguments instead
+Warning: Arguments Scope is deprecated; use Arguments instead
+Warning: Arguments Scope is deprecated; use Arguments instead
+Warning: Arguments Scope is deprecated; use Arguments instead
+Warning: Arguments Scope is deprecated; use Arguments instead
 a : bool -> bool
 
 Expands to: Variable a
diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out
new file mode 100644
index 00000000..e443115c
--- /dev/null
+++ b/test-suite/output/Arguments_renaming.out
@@ -0,0 +1,108 @@
+The command has indeed failed with message:
+=> Error: To rename arguments the "rename" flag must be specified.
+The command has indeed failed with message:
+=> Error: To rename arguments the "rename" flag must be specified.
+@eq_refl
+     : forall (B : Type) (y : B), y = y
+eq_refl
+     : forall x : nat, x = x
+Inductive eq (A : Type) (x : A) : A -> Prop :=  eq_refl : x = x
+
+For eq_refl: Arguments are renamed to B, y
+For eq: Argument A is implicit and maximally inserted
+For eq_refl, when applied to no arguments:
+  Arguments B, y are implicit and maximally inserted
+For eq_refl, when applied to 1 argument:
+  Argument B is implicit
+For eq: Argument scopes are [type_scope _ _]
+For eq_refl: Argument scopes are [type_scope _]
+eq_refl : forall (A : Type) (x : A), x = x
+
+Arguments are renamed to B, y
+When applied to no arguments:
+  Arguments B, y are implicit and maximally inserted
+When applied to 1 argument:
+  Argument B is implicit
+Argument scopes are [type_scope _]
+Expands to: Constructor Coq.Init.Logic.eq_refl
+Inductive myEq (B : Type) (x : A) : A -> Prop :=  myrefl : B -> myEq B x x
+
+For myrefl: Arguments are renamed to C, x, _
+For myrefl: Argument C is implicit and maximally inserted
+For myEq: Argument scopes are [type_scope _ _]
+For myrefl: Argument scopes are [type_scope _ _]
+myrefl : forall (B : Type) (x : A), B -> myEq B x x
+
+Arguments are renamed to C, x, _
+Argument C is implicit and maximally inserted
+Argument scopes are [type_scope _ _]
+Expands to: Constructor Top.Test1.myrefl
+myplus = 
+fix myplus (T : Type) (t : T) (n m : nat) {struct n} : nat :=
+  match n with
+  | 0 => m
+  | S n' => S (myplus T t n' m)
+  end
+     : forall T : Type, T -> nat -> nat -> nat
+
+Arguments are renamed to Z, t, n, m
+Argument Z is implicit and maximally inserted
+Argument scopes are [type_scope _ nat_scope nat_scope]
+myplus : forall T : Type, T -> nat -> nat -> nat
+
+Arguments are renamed to Z, t, n, m
+Argument Z is implicit and maximally inserted
+Argument scopes are [type_scope _ nat_scope nat_scope]
+The simpl tactic unfolds myplus
+  when the 2nd and 3rd arguments evaluate to a constructor 
+myplus is transparent
+Expands to: Constant Top.Test1.myplus
+myplus
+     : forall Z : Type, Z -> nat -> nat -> nat
+Inductive myEq (A B : Type) (x : A) : A -> Prop :=
+    myrefl : B -> myEq A B x x
+
+For myrefl: Arguments are renamed to A, C, x, _
+For myrefl: Argument C is implicit and maximally inserted
+For myEq: Argument scopes are [type_scope type_scope _ _]
+For myrefl: Argument scopes are [type_scope type_scope _ _]
+myrefl : forall (A B : Type) (x : A), B -> myEq A B x x
+
+Arguments are renamed to A, C, x, _
+Argument C is implicit and maximally inserted
+Argument scopes are [type_scope type_scope _ _]
+Expands to: Constructor Top.myrefl
+myrefl
+     : forall (A C : Type) (x : A), C -> myEq A C x x
+myplus = 
+fix myplus (T : Type) (t : T) (n m : nat) {struct n} : nat :=
+  match n with
+  | 0 => m
+  | S n' => S (myplus T t n' m)
+  end
+     : forall T : Type, T -> nat -> nat -> nat
+
+Arguments are renamed to Z, t, n, m
+Argument Z is implicit and maximally inserted
+Argument scopes are [type_scope _ nat_scope nat_scope]
+myplus : forall T : Type, T -> nat -> nat -> nat
+
+Arguments are renamed to Z, t, n, m
+Argument Z is implicit and maximally inserted
+Argument scopes are [type_scope _ nat_scope nat_scope]
+The simpl tactic unfolds myplus
+  when the 2nd and 3rd arguments evaluate to a constructor 
+myplus is transparent
+Expands to: Constant Top.myplus
+myplus
+     : forall Z : Type, Z -> nat -> nat -> nat
+The command has indeed failed with message:
+=> Error: All arguments lists must declare the same names.
+The command has indeed failed with message:
+=> Error: The following arguments are not declared: x.
+The command has indeed failed with message:
+=> Error: Arguments names must be distinct.
+The command has indeed failed with message:
+=> Error: Argument z cannot be declared implicit.
+The command has indeed failed with message:
+=> Error: Extra argument y.
diff --git a/test-suite/output/Arguments_renaming.v b/test-suite/output/Arguments_renaming.v
new file mode 100644
index 00000000..b133e733
--- /dev/null
+++ b/test-suite/output/Arguments_renaming.v
@@ -0,0 +1,54 @@
+Fail Arguments eq_refl {B y}, [B] y.
+Fail Arguments identity T _ _.
+Arguments eq_refl A x.
+Arguments eq_refl {B y}, [B] y : rename.
+
+Check @eq_refl.
+Check (eq_refl (B := nat)).
+Print eq_refl.
+About eq_refl.
+
+Goal 3 = 3.
+apply @eq_refl with (B := nat).
+Undo.
+apply @eq_refl with (y := 3).
+Undo.
+pose (y := nat).
+apply (@eq_refl y) with (y0 := 3).
+Qed.
+
+Section Test1.
+
+Variable A : Type.
+
+Inductive myEq B (x : A) : A -> Prop := myrefl : B -> myEq B x x.
+
+Global Arguments myrefl {C} x _ : rename.
+Print myrefl.
+About myrefl.
+
+Fixpoint myplus T (t : T) (n m : nat) {struct n} :=
+  match n with O => m | S n' => S (myplus T t n' m) end.
+
+Global Arguments myplus {Z} !t !n m : rename.
+
+Print myplus.
+About myplus.
+Check @myplus.
+
+End Test1.
+Print myrefl.
+About myrefl.
+Check myrefl.
+
+Print myplus.
+About myplus.
+Check @myplus.
+
+Fail Arguments eq_refl {F g}, [H] k.
+Fail Arguments eq_refl {F}, [F].
+Fail Arguments eq_refl {F F}, [F] F.
+Fail Arguments eq {F} x [z].
+Fail Arguments eq {F} x z y.
+
+
diff --git a/test-suite/output/Errors.out b/test-suite/output/Errors.out
new file mode 100644
index 00000000..f61b7ecf
--- /dev/null
+++ b/test-suite/output/Errors.out
@@ -0,0 +1,2 @@
+The command has indeed failed with message:
+=> Error: The field t is missing in Top.M.
diff --git a/test-suite/output/Errors.v b/test-suite/output/Errors.v
new file mode 100644
index 00000000..75763f3b
--- /dev/null
+++ b/test-suite/output/Errors.v
@@ -0,0 +1,9 @@
+(* Test error messages *)
+
+(* Test non-regression of bug fixed in r13486 (bad printer for module names) *)
+
+Module Type S.
+Parameter t:Type.
+End S.
+Module M : S.
+Fail End M.
diff --git a/test-suite/output/Existentials.out b/test-suite/output/Existentials.out
index ca79ba69..2f756cbb 100644
--- a/test-suite/output/Existentials.out
+++ b/test-suite/output/Existentials.out
@@ -1 +1,3 @@
-Existential 1 = ?9 : [n : nat  m : nat |- nat] 
+Existential 1 = ?10 : [q : nat  n : nat  m : nat |- n = ?9] 
+Existential 2 = ?9 : [n : nat  m : nat |- nat] 
+Existential 3 = ?7 : [p : nat  q := S p : nat  n : nat  m : nat |- ?9 = m] 
diff --git a/test-suite/output/Fixpoint.out b/test-suite/output/Fixpoint.out
index c69d31f4..a13ae462 100644
--- a/test-suite/output/Fixpoint.out
+++ b/test-suite/output/Fixpoint.out
@@ -9,17 +9,4 @@ let fix f (m : nat) : nat := match m with
                              | S m' => f m'
                              end in f 0
      : nat
-fix even_pos_odd_pos 2
- with (odd_pos_even_pos (n:_) (H:odd n) {struct H} : n >= 1).
- intros.
- destruct H.
-  omega.
-  
-  apply odd_pos_even_pos in H.
-  omega.
-  
- intros.
- destruct H.
- apply even_pos_odd_pos in H.
- omega.
- 
+Ltac f id1 id2 := fix id1 2 with (id2 (n:_) (H:odd n) {struct H} : n >= 1)
diff --git a/test-suite/output/Fixpoint.v b/test-suite/output/Fixpoint.v
index af5f05f6..8afa50ba 100644
--- a/test-suite/output/Fixpoint.v
+++ b/test-suite/output/Fixpoint.v
@@ -25,6 +25,11 @@ Inductive even: Z -> Prop :=
 with odd: Z -> Prop :=
 | odd_succ: forall n, even (n - 1) -> odd n.
 
+(* Check printing of fix *)
+Ltac f id1 id2 := fix id1 2 with (id2 n (H:odd n) {struct H} : n >= 1).
+Print Ltac f.
+
+(* Incidentally check use of fix in proofs *)
 Lemma even_pos_odd_pos: forall n, even n -> n >= 0.
 Proof.
 fix even_pos_odd_pos 2 with (odd_pos_even_pos n (H:odd n) {struct H} : n >= 1).
@@ -37,5 +42,6 @@ fix even_pos_odd_pos 2 with (odd_pos_even_pos n (H:odd n) {struct H} : n >= 1).
  destruct H.
   apply even_pos_odd_pos in H.
   omega.
-Show Script.
 Qed.
+
+
diff --git a/test-suite/output/Implicit.out b/test-suite/output/Implicit.out
index ecfe8505..3b65003c 100644
--- a/test-suite/output/Implicit.out
+++ b/test-suite/output/Implicit.out
@@ -11,3 +11,5 @@ map id (1 :: nil)
      : list nat
 map id' (1 :: nil)
      : list nat
+map (id'' (A:=nat)) (1 :: nil)
+     : list nat
diff --git a/test-suite/output/Implicit.v b/test-suite/output/Implicit.v
index 4c6f2b5d..7c9b89f9 100644
--- a/test-suite/output/Implicit.v
+++ b/test-suite/output/Implicit.v
@@ -18,6 +18,9 @@ Definition d2 x := d1 (y:=x).
 
 Print d2.
 
+Set Strict Implicit.
+Unset Implicit Arguments.
+
 (* Check maximal insertion of implicit *)
 
 Require Import List.
@@ -33,6 +36,18 @@ Check map id (1::nil).
 
 Definition id' (A:Type) (x:A) := x.
 
-Implicit Arguments id' [[A]].
+Arguments id' {A} x.
 
 Check map id' (1::nil).
+
+Unset Maximal Implicit Insertion.
+Unset Implicit Arguments.
+
+(* Check explicit insertion of last non-maximal trailing implicit to ensure *)
+(* correct arity of partiol applications *)
+
+Set Implicit Arguments.
+Definition id'' (A:Type) (x:A) := x.
+
+Check map (@id'' nat) (1::nil).
+
diff --git a/test-suite/output/InitSyntax.out b/test-suite/output/InitSyntax.out
index 9299e010..55017469 100644
--- a/test-suite/output/InitSyntax.out
+++ b/test-suite/output/InitSyntax.out
@@ -1,5 +1,5 @@
 Inductive sig2 (A : Type) (P Q : A -> Prop) : Type :=
-    exist2 : forall x : A, P x -> Q x -> sig2 P Q
+    exist2 : forall x : A, P x -> Q x -> {x | P x & Q x}
 
 For sig2: Argument A is implicit
 For exist2: Argument A is implicit
diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out
index 215d9b68..ada524f1 100644
--- a/test-suite/output/Notations.out
+++ b/test-suite/output/Notations.out
@@ -2,10 +2,10 @@ true ? 0; 1
      : nat
 if true as x return (x ? nat; bool) then 0 else true
      : nat
-Defining 'proj1' as keyword
+Identifier 'proj1' now a keyword
 fun e : nat * nat => proj1 e
      : nat * nat -> nat
-Defining 'decomp' as keyword
+Identifier 'decomp' now a keyword
 decomp (true, true) as t, u in (t, u)
      : bool * bool
 !(0 = 0)
@@ -28,18 +28,18 @@ forall n n0 : nat, ###(n = n0)
      : list nat
 (1; 2, 4)
      : nat * nat * nat
-Defining 'ifzero' as keyword
+Identifier 'ifzero' now a keyword
 ifzero 3
      : bool
-Defining 'pred' as keyword
+Identifier 'pred' now a keyword
 pred 3
      : nat
 fun n : nat => pred n
      : nat -> nat
 fun n : nat => pred n
      : nat -> nat
-Defining 'ifn' as keyword
-Defining 'is' as keyword
+Identifier 'ifn' now a keyword
+Identifier 'is' now a keyword
 fun x : nat => ifn x is succ n then n else 0
      : nat -> nat
 1-
@@ -80,7 +80,7 @@ Nil
      : forall A : Type, list A
 NIL:list nat
      : list nat
-Defining 'I' as keyword
+Identifier 'I' now a keyword
 (false && I 3)%bool /\ I 6
      : Prop
 [|1, 2, 3; 4, 5, 6|]
@@ -120,3 +120,5 @@ fun x : option Z => match x with
                     | NONE3 => 0
                     end
      : option Z -> Z
+s
+     : s
diff --git a/test-suite/output/Notations.v b/test-suite/output/Notations.v
index b8f8f48f..4a2c411e 100644
--- a/test-suite/output/Notations.v
+++ b/test-suite/output/Notations.v
@@ -245,3 +245,11 @@ Check (fun x => match x with SOME2 x => x | NONE2 => 0 end).
 Notation NONE3 := @None.
 Notation SOME3 := @Some.     
 Check (fun x => match x with SOME3 x => x | NONE3 => 0 end).
+
+(* Check correct matching of "Type" in notations. Of course the
+   notation denotes a term that will be reinterpreted with a different
+   universe than the actual one; but it would be the same anyway
+   without a notation *)
+
+Notation s := Type.
+Check s.
diff --git a/test-suite/output/Notations2.out b/test-suite/output/Notations2.out
index 6731d505..47741e43 100644
--- a/test-suite/output/Notations2.out
+++ b/test-suite/output/Notations2.out
@@ -10,10 +10,19 @@ end
      : nat
 let '(a, _, _) := (2, 3, 4) in a
      : nat
+fun (P : nat -> nat -> Prop) (x : nat) => exists x0, P x x0
+     : (nat -> nat -> Prop) -> nat -> Prop
 ∃ n p : nat, n + p = 0
      : Prop
+let a := 0 in
+∃ x y : nat,
+let b := 1 in
+let c := b in
+let d := 2 in ∃ z : nat, let e := 3 in let f := 4 in x + y = z + d
+     : Prop
 ∀ n p : nat, n + p = 0
      : Prop
+Identifier 'λ' now a keyword
 λ n p : nat, n + p = 0
      : nat -> nat -> Prop
 λ (A : Type) (n p : A), n = p
@@ -22,6 +31,18 @@ let '(a, _, _) := (2, 3, 4) in a
      : Type -> Prop
 λ A : Type, ∀ n p : A, n = p
      : Type -> Prop
-Defining 'let'' as keyword
-let' f (x y z : nat) (_ : bool) := x + y + z + 1 in f 0 1 2
+Identifier 'let'' now a keyword
+let' f (x y : nat) (a:=0) (z : nat) (_ : bool) := x + y + z + 1 in f 0 1 2
      : bool -> nat
+λ (f : nat -> nat) (x : nat), f(x) + S(x)
+     : (nat -> nat) -> nat -> nat
+Notation plus2 n := (S (S n))
+λ n : list(nat),
+match n with
+| nil => 2
+| 0 :: _ => 2
+| list1 => 0
+| 1 :: _ :: _ => 2
+| plus2 _ :: _ => 2
+end
+     : list(nat) -> nat
diff --git a/test-suite/output/Notations2.v b/test-suite/output/Notations2.v
index 57d8ebbc..e902a3c2 100644
--- a/test-suite/output/Notations2.v
+++ b/test-suite/output/Notations2.v
@@ -25,19 +25,25 @@ Remove Printing Let prod.
 Check match (0,0,0) with (x,y,z) => x+y+z end.
 Check let '(a,b,c) := ((2,3),4) in a.
 
+(* Test notation for anonymous functions up to eta-expansion *)
+
+Check fun P:nat->nat->Prop => fun x:nat => ex (P x). 
+
 (* Test notations with binders *)
 
-Notation "∃  x .. y , P":=
-  (ex (fun x => .. (ex (fun y => P)) ..)) (x binder, y binder, at level 200).
+Notation "∃  x .. y , P":= (ex (fun x => .. (ex (fun y => P)) ..))
+  (x binder, y binder, at level 200, right associativity).
 
 Check (∃ n p, n+p=0).
 
+Check ∃ (a:=0) (x:nat) y (b:=1) (c:=b) (d:=2) z (e:=3) (f:=4), x+y = z+d.
+
 Notation "∀  x .. y , P":= (forall x, .. (forall y, P) ..)
   (x binder, at level 200, right associativity).
 
 Check (∀ n p, n+p=0).
 
-Notation "'λ'  x .. y , P":= (fun x, .. (fun y, P) ..)
+Notation "'λ'  x .. y , P":= (fun x => .. (fun y => P) ..)
   (y binder, at level 200, right associativity).
 
 Check (λ n p, n+p=0).
@@ -53,7 +59,19 @@ Notation "'let'' f x .. y  :=  t 'in' u":=
   (f ident, x closed binder, y closed binder, at level 200,
    right associativity).
 
-Check let' f x y z (a:bool) := x+y+z+1 in f 0 1 2.
+Check let' f x y (a:=0) z (b:bool) := x+y+z+1 in f 0 1 2.
+
+(* In practice, only the printing rule is used here *)
+(* Note: does not work for pattern *)
+Notation "f ( x )" := (f x) (at level 10, format "f ( x )").
+Check fun f x => f x + S x.
+
+Open Scope list_scope.
+Notation list1 := (1::nil)%list.
+Notation plus2 n := (S (S n)).
+(* plus2 was not correctly printed in the two following tests in 8.3pl1 *)
+Print plus2.
+Check fun n => match n with list1 => 0 | _ => 2 end.
 
 (* This one is not fully satisfactory because binders in the same type
    are re-factorized and parentheses are needed even for atomic binder
diff --git a/test-suite/output/NumbersSyntax.out b/test-suite/output/NumbersSyntax.out
index b2a44fb7..b2677b6a 100644
--- a/test-suite/output/NumbersSyntax.out
+++ b/test-suite/output/NumbersSyntax.out
@@ -13,19 +13,19 @@ I31
      = 710436486
      : int31
 2
-     : BigN.t_
+     : BigN.t'
 1000000000000000000
-     : BigN.t_
+     : BigN.t'
 2 + 2
-     : BigN.t_
+     : bigN
 2 + 2
-     : BigN.t_
+     : bigN
      = 4
-     : BigN.t_
+     : bigN
      = 37151199385380486
-     : BigN.t_
+     : bigN
      = 1267650600228229401496703205376
-     : BigN.t_
+     : bigN
 2
      : BigZ.t_
 -1000000000000000000
diff --git a/test-suite/output/PrintInfos.out b/test-suite/output/PrintInfos.out
new file mode 100644
index 00000000..40c786ab
--- /dev/null
+++ b/test-suite/output/PrintInfos.out
@@ -0,0 +1,129 @@
+existT : forall (A : Type) (P : A -> Type) (x : A), P x -> sigT P
+
+Argument A is implicit
+Argument scopes are [type_scope _ _ _]
+Expands to: Constructor Coq.Init.Specif.existT
+Inductive sigT (A : Type) (P : A -> Type) : Type :=
+    existT : forall x : A, P x -> sigT P
+
+For sigT: Argument A is implicit
+For existT: Argument A is implicit
+For sigT: Argument scopes are [type_scope type_scope]
+For existT: Argument scopes are [type_scope _ _ _]
+existT : forall (A : Type) (P : A -> Type) (x : A), P x -> sigT P
+
+Argument A is implicit
+Inductive eq (A : Type) (x : A) : A -> Prop :=  eq_refl : x = x
+
+For eq: Argument A is implicit and maximally inserted
+For eq_refl, when applied to no arguments:
+  Arguments A, x are implicit and maximally inserted
+For eq_refl, when applied to 1 argument:
+  Argument A is implicit
+For eq: Argument scopes are [type_scope _ _]
+For eq_refl: Argument scopes are [type_scope _]
+eq_refl : forall (A : Type) (x : A), x = x
+
+When applied to no arguments:
+  Arguments A, x are implicit and maximally inserted
+When applied to 1 argument:
+  Argument A is implicit
+Argument scopes are [type_scope _]
+Expands to: Constructor Coq.Init.Logic.eq_refl
+eq_refl : forall (A : Type) (x : A), x = x
+
+When applied to no arguments:
+  Arguments A, x are implicit and maximally inserted
+When applied to 1 argument:
+  Argument A is implicit
+plus = 
+fix plus (n m : nat) : nat := match n with
+                              | 0 => m
+                              | S p => S (plus p m)
+                              end
+     : nat -> nat -> nat
+
+Argument scopes are [nat_scope nat_scope]
+plus : nat -> nat -> nat
+
+Argument scopes are [nat_scope nat_scope]
+plus is transparent
+Expands to: Constant Coq.Init.Peano.plus
+plus : nat -> nat -> nat
+
+plus_n_O : forall n : nat, n = n + 0
+
+Argument scope is [nat_scope]
+plus_n_O is opaque
+Expands to: Constant Coq.Init.Peano.plus_n_O
+Warning: Implicit Arguments is deprecated; use Arguments instead
+Inductive le (n : nat) : nat -> Prop :=
+    le_n : n <= n | le_S : forall m : nat, n <= m -> n <= S m
+
+For le_S: Argument m is implicit
+For le_S: Argument n is implicit and maximally inserted
+For le: Argument scopes are [nat_scope nat_scope]
+For le_n: Argument scope is [nat_scope]
+For le_S: Argument scopes are [nat_scope nat_scope _]
+Inductive le (n : nat) : nat -> Prop :=
+    le_n : n <= n | le_S : forall m : nat, n <= m -> n <= S m
+
+For le_S: Argument m is implicit
+For le_S: Argument n is implicit and maximally inserted
+For le: Argument scopes are [nat_scope nat_scope]
+For le_n: Argument scope is [nat_scope]
+For le_S: Argument scopes are [nat_scope nat_scope _]
+comparison : Set
+
+Expands to: Inductive Coq.Init.Datatypes.comparison
+Inductive comparison : Set :=
+    Eq : comparison | Lt : comparison | Gt : comparison
+Warning: Implicit Arguments is deprecated; use Arguments instead
+bar : foo
+
+Expanded type for implicit arguments
+bar : forall x : nat, x = 0
+
+Argument x is implicit and maximally inserted
+Expands to: Constant Top.bar
+*** [ bar : foo ]
+
+Expanded type for implicit arguments
+bar : forall x : nat, x = 0
+
+Argument x is implicit and maximally inserted
+bar : foo
+
+Expanded type for implicit arguments
+bar : forall x : nat, x = 0
+
+Argument x is implicit and maximally inserted
+Expands to: Constant Top.bar
+*** [ bar : foo ]
+
+Expanded type for implicit arguments
+bar : forall x : nat, x = 0
+
+Argument x is implicit and maximally inserted
+Module Coq.Init.Peano
+Notation existS2 := existT2
+Expands to: Notation Coq.Init.Specif.existS2
+Warning: Implicit Arguments is deprecated; use Arguments instead
+Inductive eq (A : Type) (x : A) : A -> Prop :=  eq_refl : x = x
+
+For eq: Argument A is implicit and maximally inserted
+For eq_refl, when applied to no arguments:
+  Arguments A, x are implicit and maximally inserted
+For eq_refl, when applied to 1 argument:
+  Argument A is implicit and maximally inserted
+For eq: Argument scopes are [type_scope _ _]
+For eq_refl: Argument scopes are [type_scope _]
+Inductive eq (A : Type) (x : A) : A -> Prop :=  eq_refl : x = x
+
+For eq: Argument A is implicit and maximally inserted
+For eq_refl, when applied to no arguments:
+  Arguments A, x are implicit and maximally inserted
+For eq_refl, when applied to 1 argument:
+  Argument A is implicit and maximally inserted
+For eq: Argument scopes are [type_scope _ _]
+For eq_refl: Argument scopes are [type_scope _]
diff --git a/test-suite/output/PrintInfos.v b/test-suite/output/PrintInfos.v
new file mode 100644
index 00000000..deeb1f65
--- /dev/null
+++ b/test-suite/output/PrintInfos.v
@@ -0,0 +1,41 @@
+About existT.
+Print existT.
+Print Implicit existT.
+
+Print eq_refl.
+About eq_refl.
+Print Implicit eq_refl.
+
+Print plus.
+About plus.
+Print Implicit plus.
+
+About plus_n_O.
+
+Implicit Arguments le_S [[n] m].
+Print le_S.
+
+Arguments le_S {n} [m] _. (* Test new syntax *)
+Print le_S.
+
+About comparison.
+Print comparison.
+
+Definition foo := forall x, x = 0.
+Parameter bar : foo.
+Implicit Arguments bar [x].
+About bar.
+Print bar.
+
+Arguments bar [x]. (* Test new syntax *)
+About bar.
+Print bar.
+
+About Peano. (* Module *)
+About existS2. (* Notation *)
+
+Implicit Arguments eq_refl [[A] [x]] [[A]].
+Print eq_refl.
+
+Arguments eq_refl {A} {x}, {A} x. (* Test new syntax *)
+Print eq_refl.
diff --git a/test-suite/output/Record.out b/test-suite/output/Record.out
new file mode 100644
index 00000000..36d643a4
--- /dev/null
+++ b/test-suite/output/Record.out
@@ -0,0 +1,16 @@
+{| field := 5 |}
+     : test
+{| field := 5 |}
+     : test
+{| field_r := 5 |}
+     : test_r
+build_c 5
+     : test_c
+build 5
+     : test
+build 5
+     : test
+{| field_r := 5 |}
+     : test_r
+build_c 5
+     : test_c
diff --git a/test-suite/output/Record.v b/test-suite/output/Record.v
new file mode 100644
index 00000000..6aa3df98
--- /dev/null
+++ b/test-suite/output/Record.v
@@ -0,0 +1,21 @@
+Record test := build { field : nat }.
+Record test_r := build_r { field_r : nat }.
+Record test_c := build_c { field_c : nat }.
+
+Add Printing Constructor test_c.
+Add Printing Record test_r.
+
+Set Printing Records.
+
+Check build 5.
+Check {| field := 5 |}.
+
+Check build_r 5.
+Check build_c 5.
+
+Unset Printing Records.
+
+Check build 5.
+Check {| field := 5 |}.
+Check build_r 5.
+Check build_c 5.
diff --git a/test-suite/output/Search.out b/test-suite/output/Search.out
index 154d9cdd..5d8f98ed 100644
--- a/test-suite/output/Search.out
+++ b/test-suite/output/Search.out
@@ -1,5 +1,7 @@
 le_S: forall n m : nat, n <= m -> n <= S m
 le_n: forall n : nat, n <= n
+le_pred: forall n m : nat, n <= m -> pred n <= pred m
+le_S_n: forall n m : nat, S n <= S m -> n <= m
 false: bool
 true: bool
 xorb: bool -> bool -> bool
@@ -14,5 +16,9 @@ plus_Sn_m: forall n m : nat, S n + m = S (n + m)
 plus_O_n: forall n : nat, 0 + n = n
 mult_n_Sm: forall n m : nat, n * m + n = n * S m
 mult_n_O: forall n : nat, 0 = n * 0
+min_r: forall n m : nat, m <= n -> min n m = m
+min_l: forall n m : nat, n <= m -> min n m = n
+max_r: forall n m : nat, n <= m -> max n m = m
+max_l: forall n m : nat, m <= n -> max n m = n
 eq_add_S: forall n m : nat, S n = S m -> n = m
 eq_S: forall x y : nat, x = y -> S x = S y
diff --git a/test-suite/output/SearchPattern.out b/test-suite/output/SearchPattern.out
index c87eaadc..9106a4e3 100644
--- a/test-suite/output/SearchPattern.out
+++ b/test-suite/output/SearchPattern.out
@@ -11,16 +11,20 @@ pred: nat -> nat
 plus: nat -> nat -> nat
 mult: nat -> nat -> nat
 minus: nat -> nat -> nat
+min: nat -> nat -> nat
+max: nat -> nat -> nat
 length: forall A : Type, list A -> nat
 S: nat -> nat
 pred: nat -> nat
 plus: nat -> nat -> nat
 mult: nat -> nat -> nat
 minus: nat -> nat -> nat
+min: nat -> nat -> nat
+max: nat -> nat -> nat
 mult_n_Sm: forall n m : nat, n * m + n = n * S m
 le_n: forall n : nat, n <= n
-eq_refl: forall (A : Type) (x : A), x = x
 identity_refl: forall (A : Type) (a : A), identity a a
+eq_refl: forall (A : Type) (x : A), x = x
 iff_refl: forall A : Prop, A <-> A
-conj: forall A B : Prop, A -> B -> A /\ B
 pair: forall A B : Type, A -> B -> A * B
+conj: forall A B : Prop, A -> B -> A /\ B
diff --git a/test-suite/output/Tactics.out b/test-suite/output/Tactics.out
index ac5eedc1..9949658c 100644
--- a/test-suite/output/Tactics.out
+++ b/test-suite/output/Tactics.out
@@ -1,6 +1,4 @@
-intro H; split; [ a H | e H ].
-
-intros; match goal with
-        | |- context [if ?X then _ else _] => case X
-        end; trivial.
-
+Ltac f H := split; [ a H | e H ]
+Ltac g := match goal with
+          | |- context [if ?X then _ else _] => case X
+          end
diff --git a/test-suite/output/Tactics.v b/test-suite/output/Tactics.v
index 8fa91994..a7c497cf 100644
--- a/test-suite/output/Tactics.v
+++ b/test-suite/output/Tactics.v
@@ -3,16 +3,11 @@
 Tactic Notation "a" constr(x) := apply x.
 Tactic Notation "e" constr(x) := exact x.
 
-Lemma test : True -> True /\ True.
-intro H; split; [a H|e H].
-Show Script.
-Qed.
+Ltac f H := split; [a H|e H].
+Print Ltac f.
 
 (* Test printing of match context *)
 (* Used to fail after translator removal (see bug #1070) *)
 
-Lemma test2 : forall n:nat, forall f: nat -> bool, O = if (f n) then O else O.
-Proof.
-intros;match goal with |- context [if ?X then _ else _ ] => case X end;trivial.
-Show Script.
-Qed.
+Ltac g := match goal with |- context [if ?X then _ else _ ] => case X end.
+Print Ltac g.
diff --git a/test-suite/output/ZSyntax.out b/test-suite/output/ZSyntax.out
index f23198b0..1b7a2903 100644
--- a/test-suite/output/ZSyntax.out
+++ b/test-suite/output/ZSyntax.out
@@ -16,11 +16,11 @@ fun x : positive => (- Zpos x~0)%Z
      : positive -> Z
 fun x : positive => (- Zpos x~0 + 0)%Z
      : positive -> Z
-(Z_of_nat 0 + 1)%Z
+(Z.of_nat 0 + 1)%Z
      : Z
-(0 + Z_of_nat (0 + 0))%Z
+(0 + Z.of_nat (0 + 0))%Z
      : Z
-Z_of_nat 0 = 0%Z
+Z.of_nat 0 = 0%Z
      : Prop
-(0 + Z_of_nat 11)%Z
+(0 + Z.of_nat 11)%Z
      : Z
diff --git a/test-suite/output/ZSyntax.v b/test-suite/output/ZSyntax.v
index 289a1e3f..d3640cae 100644
--- a/test-suite/output/ZSyntax.v
+++ b/test-suite/output/ZSyntax.v
@@ -8,10 +8,10 @@ Check (fun x : positive => Zneg (xO x)).
 Check (fun x : positive => (Zpos (xO x) + 0)%Z).
 Check (fun x : positive => (- Zpos (xO x))%Z).
 Check (fun x : positive => (- Zpos (xO x) + 0)%Z).
-Check (Z_of_nat 0 + 1)%Z.
-Check (0 + Z_of_nat (0 + 0))%Z.
-Check (Z_of_nat 0 = 0%Z).
+Check (Z.of_nat 0 + 1)%Z.
+Check (0 + Z.of_nat (0 + 0))%Z.
+Check (Z.of_nat 0 = 0%Z).
 
 (* Submitted by Pierre Casteran *)
 Require Import Arith.
-Check (0 + Z_of_nat 11)%Z.
+Check (0 + Z.of_nat 11)%Z.
diff --git a/test-suite/output/inference.out b/test-suite/output/inference.out
new file mode 100644
index 00000000..bca3b361
--- /dev/null
+++ b/test-suite/output/inference.out
@@ -0,0 +1,6 @@
+P = 
+fun e : option L => match e with
+                    | Some cl => Some cl
+                    | None => None
+                    end
+     : option L -> option L
diff --git a/test-suite/output/inference.v b/test-suite/output/inference.v
new file mode 100644
index 00000000..968ea71a
--- /dev/null
+++ b/test-suite/output/inference.v
@@ -0,0 +1,14 @@
+(* Check that types are not uselessly unfolded *)
+
+(* Check here that P returns something of type "option L" and not
+   "option (list nat)" *)
+
+Definition L := list nat.
+
+Definition P (e:option L) :=
+  match e with
+  | None => None
+  | Some cl => Some cl
+  end.
+
+Print P.
diff --git a/test-suite/output/rewrite-2172.out b/test-suite/output/rewrite-2172.out
new file mode 100644
index 00000000..30385072
--- /dev/null
+++ b/test-suite/output/rewrite-2172.out
@@ -0,0 +1,2 @@
+The command has indeed failed with message:
+=> Error: Unable to find an instance for the variable E.
diff --git a/test-suite/output/rewrite-2172.v b/test-suite/output/rewrite-2172.v
new file mode 100644
index 00000000..212b1c12
--- /dev/null
+++ b/test-suite/output/rewrite-2172.v
@@ -0,0 +1,21 @@
+(* This checks an error message as reported in bug #2172 *)
+
+Axiom axiom : forall (E F : nat), E = F.
+Lemma test : forall (E F : nat), E = F.
+Proof.
+  intros.
+(* This used to raise the following non understandable error message:
+
+   Error: Unable to find an instance for the variable x
+
+   The reason this error was that rewrite generated the proof
+
+   "eq_ind ?A ?x ?P ? ?y (axiom ?E ?F)"
+
+   and the equation ?x=?E was solved in the way ?E:=?x leaving ?x
+   unresolved. A stupid hack for solve this consisted in ordering
+   meta=meta equations the other way round (with most recent evars
+   instantiated first - since they are assumed to come first from the
+   user in rewrite/induction/destruct calls).
+*)
+  Fail rewrite <- axiom.
diff --git a/test-suite/success/AdvancedCanonicalStructure.v b/test-suite/success/AdvancedCanonicalStructure.v
index b533db6e..97cf316c 100644
--- a/test-suite/success/AdvancedCanonicalStructure.v
+++ b/test-suite/success/AdvancedCanonicalStructure.v
@@ -79,19 +79,17 @@ Record interp_pair :Type :=
     link: abs = interp repr }.
 
 Lemma prod_interp :forall (a b:interp_pair),a * b = interp (Prod a b) .
-proof.
-let a:interp_pair,b:interp_pair.
-reconsider thesis as (a * b = interp a * interp b).
-thus thesis by (link a),(link b).
-end proof.
+Proof.
+intros a b.
+change (a * b = interp a * interp b).
+rewrite (link a), (link b); reflexivity.
 Qed.
 
 Lemma fun_interp :forall (a b:interp_pair), (a -> b) = interp (Fun a b).
-proof.
-let a:interp_pair,b:interp_pair.
-reconsider thesis as ((a -> b) = (interp a -> interp b)).
-thus thesis using rewrite (link a);rewrite (link b);reflexivity.
-end proof.
+Proof.
+intros a b.
+change ((a -> b) = (interp a -> interp b)).
+rewrite (link a), (link b); reflexivity.
 Qed.
 
 Canonical Structure ProdCan (a b:interp_pair) :=
diff --git a/test-suite/success/CaseAlias.v b/test-suite/success/CaseAlias.v
index 32d85779..a9249086 100644
--- a/test-suite/success/CaseAlias.v
+++ b/test-suite/success/CaseAlias.v
@@ -1,3 +1,4 @@
+(*********************************************)
 (* This has been a bug reported by Y. Bertot *)
 Inductive expr : Set :=
   | b : expr -> expr -> expr
@@ -19,3 +20,72 @@ Fixpoint f2 (t : expr) : expr :=
   | x => b x a
   end.
 
+(*********************************************)
+(* Test expansion of aliases                 *)
+(* Originally taken from NMake_gen.v         *)
+
+ Local Notation SizePlus n := (S (S (S (S (S (S n)))))).
+ Local Notation Size := (SizePlus O).
+
+ Parameter zn2z : Type -> Type.
+ Parameter w0 : Type.
+ Fixpoint word (w : Type) (n : nat) {struct n} : Type :=
+  match n with
+  | 0 => w
+  | S n0 => zn2z (word w n0)
+  end.
+
+ Definition w1 := zn2z w0.
+ Definition w2 := zn2z w1.
+ Definition w3 := zn2z w2.
+ Definition w4 := zn2z w3.
+ Definition w5 := zn2z w4.
+ Definition w6 := zn2z w5.
+
+ Definition dom_t n := match n with
+  | 0 => w0
+  | 1 => w1
+  | 2 => w2
+  | 3 => w3
+  | 4 => w4
+  | 5 => w5
+  | 6 => w6
+  | SizePlus n => word w6 n
+ end.
+Parameter plus_t : forall n m : nat, word (dom_t n) m -> dom_t (m + n).
+
+(* This used to fail because of a bug in expansion of SizePlus wrongly
+   reusing n as an alias for the subpattern *)
+Definition plus_t1 n : forall m, word (dom_t n) m -> dom_t (m+n) :=
+   match n return (forall m, word (dom_t n) m -> dom_t (m+n)) with
+     | SizePlus (S n') as n => plus_t n
+     | _ as n =>
+         fun m => match m return (word (dom_t n) m -> dom_t (m+n)) with
+                    | SizePlus (S (S m')) as m => plus_t n m
+                    | _ => fun x => x
+                  end
+   end.
+
+(* Test (useless) intermediate alias *)
+Definition plus_t2 n : forall m, word (dom_t n) m -> dom_t (m+n) :=
+   match n return (forall m, word (dom_t n) m -> dom_t (m+n)) with
+     | S (S (S (S (S (S (S n'))))) as n) as n'' => plus_t n''
+     | _ as n =>
+         fun m => match m return (word (dom_t n) m -> dom_t (m+n)) with
+                    | SizePlus (S (S m')) as m => plus_t n m
+                    | _ => fun x => x
+                  end
+   end.
+
+(*****************************************************************************)
+(* Check that alias expansion behaves consistently from versions to versions *)
+
+Definition g m :=
+  match pred m with
+  | 0 => 0
+  | n => n (* For compatibility, right-hand side should be (S n), not (pred m) *)
+  end.
+
+Goal forall m, g m = match pred m with 0 => 0 | S n => S n end.
+intro; reflexivity.
+Abort.
diff --git a/test-suite/success/Cases.v b/test-suite/success/Cases.v
index e63972ce..745529bf 100644
--- a/test-suite/success/Cases.v
+++ b/test-suite/success/Cases.v
@@ -543,7 +543,7 @@ Type
    end).
 
 (* Nested Cases: the SYNTH of the Cases on n used to make Multcase believe
- * it has to synthtize the predicate on O (which he can't)
+ * it has to synthesize the predicate on O (which he can't)
  *)
 Type
   match 0 as n return match n with
@@ -611,31 +611,52 @@ Type
    | Consn n a (Consn m b l) => n + m
    end).
 
-(*
-Type [A:Set][n:nat][l:(Listn A n)]
-                   <[_:nat](Listn A O)>Cases l of
-                         (Niln  as b) => b
-                      | (Consn  n a (Niln  as b))=> (Niln A)
-                      | (Consn  n a (Consn m b l)) => (Niln A)
-                      end.
-
-Type [A:Set][n:nat][l:(Listn A n)]
-                    Cases l of
-                         (Niln  as b) => b
-                      | (Consn  n a (Niln  as b))=> (Niln A)
-                      | (Consn  n a (Consn m b l)) => (Niln A)
-                      end.
+(* This example was deactivated in Cristina's code
+
+Type
+  (fun (A:Set) (n:nat) (l:Listn A n) =>
+    match l return Listn A O with
+      | Niln  as b => b
+      | Consn  n a (Niln  as b) => (Niln A)
+      | Consn  n a (Consn m b l) => (Niln A)
+    end).
+*)
+
+(* This one is (still) failing: too weak unification
+
+Type
+  (fun (A:Set) (n:nat) (l:Listn A n) =>
+    match l with
+      | Niln  as b => b
+      | Consn  n a (Niln  as b) => (Niln A)
+      | Consn  n a (Consn m b l) => (Niln A)
+    end).
+*)
+
+(* This one is failing: alias L not chosen of the right type
+
+Type
+  (fun (A:Set) (n:nat) (l:Listn A n) =>
+    match l return Listn A (S 0) with
+      | Niln  as b => Consn A O O b
+      | Consn n a Niln as L => L
+      | Consn n a _ => Consn A O O (Niln A)
+    end).
 *)
-(******** This example rises an error unconstrained_variables!
-Type [A:Set][n:nat][l:(Listn A n)]
-                    Cases l of
-                         (Niln  as b) => (Consn A O O b)
-                      | ((Consn  n a Niln) as L) =>  L
-                      | (Consn  n a _)  =>  (Consn A O O (Niln A))
-                      end.
+
+(******** This example (still) failed
+
+Type
+  (fun (A:Set) (n:nat) (l:Listn A n) =>
+    match l return Listn A (S 0) with
+      | Niln  as b => Consn A O O b
+      | Consn n a Niln as L => L
+      | Consn n a _ => Consn A O O (Niln A)
+    end).
+
 **********)
 
-(* To test tratement of as-patterns in depth *)
+(* To test treatment of as-patterns in depth *)
 Type
   (fun (A : Set) (l : List A) =>
    match l with
@@ -1064,7 +1085,7 @@ Type
    | Consn n a (Consn m b l) => fun _ : nat => n + m
    end).
 
-(* Alsos tests for multiple _ patterns *)
+(* Also tests for multiple _ patterns *)
 Type
   (fun (A : Set) (n : nat) (l : Listn A n) =>
    match l in (Listn _ n) return (Listn A n) with
@@ -1072,14 +1093,14 @@ Type
    | Consn _ _ _ as b => b
    end).
 
-(** Horrible error message!
+(** This one was said to raised once an "Horrible error message!" *)
 
-Type [A:Set][n:nat][l:(Listn A n)]
-                        Cases l of
-                        (Niln as b) => b
-                      | ((Consn _ _ _ ) as b)=>  b
-                      end.
-******)
+Type
+  (fun (A:Set) (n:nat) (l:Listn A n) =>
+   match l with
+   | Niln as b => b
+   | Consn _ _ _  as b =>  b
+   end).
 
 Type
   match niln in (listn n) return (listn n) with
diff --git a/test-suite/success/CasesDep.v b/test-suite/success/CasesDep.v
index 29721843..d3b7cf3f 100644
--- a/test-suite/success/CasesDep.v
+++ b/test-suite/success/CasesDep.v
@@ -26,6 +26,40 @@ Fixpoint foldrn (n : nat) (bs : listn B n) {struct bs} : C :=
   end.
 End Folding.
 
+(** Testing post-processing of nested dependencies *)
+
+Check fun x:{x|x=0}*nat+nat => match x with
+      | inl ((exist 0 eq_refl),0) => None
+      | _ => Some 0
+      end.
+
+Check fun x:{_:{x|x=0}|True}+nat => match x with
+      | inl (exist (exist 0 eq_refl) I) => None
+      | _ => Some 0
+      end.
+
+Check fun x:{_:{x|x=0}|True}+nat => match x with
+      | inl (exist (exist 0 eq_refl) I) => None
+      | _ => Some 0
+      end.
+
+Check fun x:{_:{x|x=0}|True}+nat => match x return option nat with
+      | inl (exist (exist 0 eq_refl) I) => None
+      | _ => Some 0
+      end.
+
+  (* the next two examples were failing from r14703 (Nov 22 2011) to r14732 *)
+  (* due to a bug in dependencies postprocessing (revealed by CoLoR) *)
+
+Check fun x:{x:nat*nat|fst x = 0 & True} => match x return option nat with
+      | exist2 (x,y) eq_refl I => None
+      end.
+
+Check fun x:{_:{x:nat*nat|fst x = 0 & True}|True}+nat => match x return option nat with
+      | inl (exist (exist2 (x,y) eq_refl I) I) => None
+      | _ => Some 0
+      end.
+
 (* -------------------------------------------------------------------- *)
 (*   Example to test patterns matching on dependent families            *)
 (* This exemple extracted from the developement done by Nacira Chabane  *)
@@ -506,3 +540,23 @@ Definition test (s:step E E) :=
     | Step nil _ (cons E nil) _ Plus l l' => true
     | _ => false
   end.
+
+(* Testing regression of bug 2454 ("get" used not be type-checkable when
+   defined with its type constraint) *)
+
+Inductive K : nat -> Type := KC : forall (p q:nat), K p.
+
+Definition get : K O -> nat := fun x => match x with KC p q => q end.
+
+(* Checking correct order of substitution of realargs *)
+(* (was broken from revision 14664 to 14669) *)
+(* Example extracted from contrib CoLoR *)
+
+Inductive EQ : nat -> nat -> Prop := R x y : EQ x y.
+
+Check fun e t (d1 d2:EQ e t) =>
+      match d1 in EQ e1 t1, d2 in EQ e2 t2 return
+        (e1,t1) = (e2,t2) -> (e1,t1) = (e,t) -> 0=0
+      with
+      | R _ _, R _ _ => fun _ _ => eq_refl
+      end.
diff --git a/test-suite/success/Check.v b/test-suite/success/Check.v
index d5b94ab4..47180ef6 100644
--- a/test-suite/success/Check.v
+++ b/test-suite/success/Check.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/test-suite/success/Discriminate.v b/test-suite/success/Discriminate.v
index dffad323..a7596741 100644
--- a/test-suite/success/Discriminate.v
+++ b/test-suite/success/Discriminate.v
@@ -32,3 +32,9 @@ intros.
 ediscriminate (H O).
 instantiate (1:=O).
 Abort.
+
+(* Check discriminate on identity *)
+
+Goal ~ identity 0 1.
+discriminate.
+Qed.
diff --git a/test-suite/success/Field.v b/test-suite/success/Field.v
index 08e8aed2..0efd90a1 100644
--- a/test-suite/success/Field.v
+++ b/test-suite/success/Field.v
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: Field.v 14641 2011-11-06 11:59:10Z herbelin $ *)
-
 (**** Tests of Field with real numbers ****)
 
 Require Import Reals RealField.
diff --git a/test-suite/success/Hints.v b/test-suite/success/Hints.v
index 4aa00e68..a93f8900 100644
--- a/test-suite/success/Hints.v
+++ b/test-suite/success/Hints.v
@@ -24,7 +24,7 @@ Hint Destruct h8 := 4 Hypothesis (_ <= _) => fun H => apply H.
 (* Checks that local names are accepted *)
 Section A.
   Remark Refl : forall (A : Set) (x : A), x = x.
-  Proof. exact refl_equal. Defined.
+  Proof. exact @refl_equal. Defined.
   Definition Sym := sym_equal.
   Let Trans := trans_equal.
 
diff --git a/test-suite/success/Inductive.v b/test-suite/success/Inductive.v
index 203fbbb7..da5dd5e4 100644
--- a/test-suite/success/Inductive.v
+++ b/test-suite/success/Inductive.v
@@ -54,6 +54,15 @@ Check
    | Build_B x0 x1 => f x0 x1
    end).
 
+(* Check inductive types with local definitions (constructors) *)
+
+Inductive I1 : Set := C1 (_:I1) (_:=0).
+
+Check (fun x:I1 =>
+  match x with
+  | C1 i n => (i,n)
+  end).
+
 (* Check implicit parameters of inductive types (submitted by Pierre
   Casteran and also implicit in #338) *)
 
@@ -78,3 +87,23 @@ Record P:Type := {PA:Set; PB:Set}.
 Definition F (p:P) := (PA p) -> (PB p).
 
 Inductive I_F:Set := c : (F (Build_P nat I_F)) -> I_F.
+
+(* Check that test for binders capturing implicit arguments is not stronger
+   than needed (problem raised by Cedric Auger) *)
+
+Set Implicit Arguments.
+Inductive bool_comp2 (b: bool): bool -> Prop :=
+| Opp2: forall q, (match b return Prop with
+                  | true => match q return Prop with 
+                              true => False |
+                              false => True end
+                  | false => match q return Prop with
+                              true => True |
+                              false => False end end) -> bool_comp2 b q.
+
+(* This one is still to be made acceptable...
+
+Set Implicit Arguments.
+Inductive I A : A->Prop := C a : (forall A, A) -> I a.
+
+ *)
diff --git a/test-suite/success/Inversion.v b/test-suite/success/Inversion.v
index 5091b44c..b068f729 100644
--- a/test-suite/success/Inversion.v
+++ b/test-suite/success/Inversion.v
@@ -73,15 +73,15 @@ Require Import Bvector.
 
 Inductive I : nat -> Set :=
   | C1 : I 1
-  | C2 : forall k i : nat, vector (I i) k -> I i.
+  | C2 : forall k i : nat, Vector.t (I i) k -> I i.
 
-Inductive SI : forall k : nat, I k -> vector nat k -> nat -> Prop :=
+Inductive SI : forall k : nat, I k -> Vector.t nat k -> nat -> Prop :=
     SC2 :
-      forall (k i vf : nat) (v : vector (I i) k) (xi : vector nat i),
+      forall (k i vf : nat) (v : Vector.t (I i) k) (xi : Vector.t nat i),
       SI (C2 v) xi vf.
 
 Theorem SUnique :
- forall (k : nat) (f : I k) (c : vector nat k) v v',
+ forall (k : nat) (f : I k) (c : Vector.t nat k) v v',
  SI f c v -> SI f c v' -> v = v'.
 Proof.
 induction 1.
@@ -129,3 +129,10 @@ Proof.
    an inconsistent state that disturbed "inversion" *)
 intros. inversion H.
 Abort.
+
+(* Bug #2314 (simplified): check that errors do not show as anomalies *)
+
+Goal True -> True.
+intro.
+Fail inversion H using False.
+Fail inversion foo using True_ind.
diff --git a/test-suite/success/LegacyField.v b/test-suite/success/LegacyField.v
index 53bcc63a..df4da431 100644
--- a/test-suite/success/LegacyField.v
+++ b/test-suite/success/LegacyField.v
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: Field.v 7693 2005-12-21 23:50:17Z herbelin $ *)
-
 (**** Tests of Field with real numbers ****)
 
 Require Import Reals LegacyRfield.
diff --git a/test-suite/success/Notations.v b/test-suite/success/Notations.v
index 661a8757..f5f5a9d1 100644
--- a/test-suite/success/Notations.v
+++ b/test-suite/success/Notations.v
@@ -59,3 +59,30 @@ Check (fun x:nat*nat => match x with R x y => (x,y) end).
 Local Notation "[ a  # ; ..  # ; b ]" := (a + .. (b + 0) ..).   
 Check [ 0 ].
 Check [ 0 # ; 1 ].
+
+(* Check well-scoping of alpha-renaming of private binders *)
+(* see bug #2248 (thanks to Marc Lasson) *)
+
+Notation "{ q , r | P }" := (fun (p:nat*nat) => let (q, r) := p in P).
+Check (fun p => {q,r| q + r = p}).
+
+(* Check that declarations of empty levels are correctly backtracked *)
+
+Section B.
+Notation "*" := 5 (at level 0) : nat_scope.
+Notation "[ h ] p" := (h + p) (at level 8, p at level 9, h at level 7) : nat_scope.
+End B.
+
+(* Should succeed *)
+Definition n := 5 * 5.
+
+(* Check that lonely notations (here FOO) do not modify the visibility
+   of scoped interpretations (bug #2634 fixed in r14819) *)
+
+Notation "x ++++ y" := (mult x y) (at level 40).
+Notation "x ++++ y" := (plus x y) : A_scope.
+Open Scope A_scope.
+Notation "'FOO' x" := (S x) (at level 40).
+Goal (2 ++++ 3) = 5.
+reflexivity.
+Abort.
diff --git a/test-suite/success/Nsatz.v b/test-suite/success/Nsatz.v
index 518d22e9..d316e4a0 100644
--- a/test-suite/success/Nsatz.v
+++ b/test-suite/success/Nsatz.v
@@ -1,51 +1,27 @@
-Require Import Nsatz ZArith Reals List Ring_polynom.
+(* compile en user    3m39.915s sur cachalot *)
+Require Import Nsatz.
 
 (* Example with a generic domain *)
 
-Variable A: Type.
-Variable Ad: Domain A.
+Section test.
 
-Definition Ari : Ring A:= (@domain_ring A Ad).
-Existing Instance Ari.
-
-Existing Instance ring_setoid.
-Existing Instance ring_plus_comp.
-Existing Instance ring_mult_comp.
-Existing Instance ring_sub_comp.
-Existing Instance ring_opp_comp.
-
-Add Ring Ar: (@ring_ring A (@domain_ring A Ad)).
-
-Instance zero_ring2 : Zero A := {zero := ring0}.
-Instance one_ring2 : One A := {one := ring1}.
-Instance addition_ring2 : Addition A := {addition x y := ring_plus x y}.
-Instance multiplication_ring2 : Multiplication A := {multiplication x y := ring_mult x y}.
-Instance subtraction_ring2 : Subtraction A := {subtraction x y := ring_sub x y}.
-Instance opposite_ring2 : Opposite A := {opposite x := ring_opp x}.
-
-Infix "==" := ring_eq (at level 70, no associativity).
-
-Ltac nsatzA := simpl; unfold Ari; nsatz_domain.
-
-Goal forall x y:A,  x == y -> x+0 == y*1+0.
-nsatzA.
-Qed.
+Context {A:Type}`{Aid:Integral_domain A}.
 
 Lemma example3 : forall x y z,
   x+y+z==0 ->
   x*y+x*z+y*z==0->
-  x*y*z==0 -> x*x*x==0.
+  x*y*z==0 -> x^3%Z==0.
 Proof.
-Time nsatzA. 
-Admitted.
+Time nsatz. 
+Qed.
 
 Lemma example4 : forall x y z u,
   x+y+z+u==0 ->
   x*y+x*z+x*u+y*z+y*u+z*u==0->
   x*y*z+x*y*u+x*z*u+y*z*u==0->
-  x*y*z*u==0 -> x*x*x*x==0.
+  x*y*z*u==0 -> x^4%Z==0.
 Proof.
-Time nsatzA.
+Time nsatz.
 Qed.
 
 Lemma example5 : forall x y z u v,
@@ -53,15 +29,17 @@ Lemma example5 : forall x y z u v,
   x*y+x*z+x*u+x*v+y*z+y*u+y*v+z*u+z*v+u*v==0->
   x*y*z+x*y*u+x*y*v+x*z*u+x*z*v+x*u*v+y*z*u+y*z*v+y*u*v+z*u*v==0->
   x*y*z*u+y*z*u*v+z*u*v*x+u*v*x*y+v*x*y*z==0 ->
-  x*y*z*u*v==0 -> x*x*x*x*x ==0.
+  x*y*z*u*v==0 -> x^5%Z==0.
 Proof.
-Time nsatzA.
+Time nsatz.
 Qed.
 
 Goal forall x y:Z,  x = y -> (x+0)%Z = (y*1+0)%Z.
 nsatz.
 Qed.
 
+Require Import Reals.
+
 Goal forall x y:R,  x = y -> (x+0)%R = (y*1+0)%R.
 nsatz.
 Qed.
@@ -70,85 +48,17 @@ Goal forall a b c x:R, a = b -> b = c -> (a*a)%R = (c*c)%R.
 nsatz.
 Qed.
 
-Section Examples.
-
-Delimit Scope PE_scope with PE.
-Infix "+" := PEadd : PE_scope.
-Infix "*" := PEmul : PE_scope.
-Infix "-" := PEsub : PE_scope.
-Infix "^" := PEpow : PE_scope.
-Notation "[ n ]" := (@PEc Z n) (at level 0).
-
-Open Scope R_scope.
-
-Lemma example1 : forall x y,
-  x+y=0 ->
-  x*y=0 ->
-  x^2=0.
-Proof.
- nsatz.
-Qed.
-
-Lemma example2 : forall x, x^2=0 -> x=0.
-Proof.
- nsatz.
-Qed.
-
-(*
-Notation X  := (PEX Z 3).
-Notation Y  := (PEX Z 2).
-Notation Z_ := (PEX Z 1).
-*)
-Lemma example3b : forall x y z,
-  x+y+z=0 ->
-  x*y+x*z+y*z=0->
-  x*y*z=0 -> x^3=0.
-Proof.
-Time nsatz. 
-Qed.
-
-(*
-Notation X  := (PEX Z 4).
-Notation Y  := (PEX Z 3).
-Notation Z_ := (PEX Z 2).
-Notation U  := (PEX Z 1).
-*)
-Lemma example4b : forall x y z u,
-  x+y+z+u=0 ->
-  x*y+x*z+x*u+y*z+y*u+z*u=0->
-  x*y*z+x*y*u+x*z*u+y*z*u=0->
-  x*y*z*u=0 -> x^4=0.
-Proof.
-Time nsatz.
-Qed.
-
-(*
-Notation x_ := (PEX Z 5).
-Notation y_ := (PEX Z 4).
-Notation z_ := (PEX Z 3).
-Notation u_ := (PEX Z 2).
-Notation v_ := (PEX Z 1).
-Notation "x :: y" := (List.cons x y)
-(at level 60, right associativity, format "'[hv' x  ::  '/' y ']'").
-Notation "x :: y" := (List.app x y)
-(at level 60, right associativity, format "x :: y").
-*)
-
-Lemma example5b : forall x y z u v,
-  x+y+z+u+v=0 ->
-  x*y+x*z+x*u+x*v+y*z+y*u+y*v+z*u+z*v+u*v=0->
-  x*y*z+x*y*u+x*y*v+x*z*u+x*z*v+x*u*v+y*z*u+y*z*v+y*u*v+z*u*v=0->
-  x*y*z*u+y*z*u*v+z*u*v*x+u*v*x*y+v*x*y*z=0 ->
-  x*y*z*u*v=0 -> x^5=0.
-Proof.
-Time nsatz.
-Qed.
-
-End Examples.
+End test.
 
 Section Geometry.
+(* See the interactive pictures of Laurent Théry 
+   on http://www-sop.inria.fr/marelle/CertiGeo/ 
+   and research paper on 
+   https://docs.google.com/fileview?id=0ByhB3nPmbnjTYzFiZmIyNGMtYTkwNC00NWFiLWJiNzEtODM4NmVkYTc2NTVk&hl=fr
+*)
 
-Open Scope R_scope.
+Require Import List.
+Require Import Reals.
 
 Record point:Type:={
  X:R;
@@ -170,60 +80,122 @@ Definition equal2(A B:point):=
   (X A)=(X B) /\ (Y A)=(Y B).
 
 Definition equal3(A B:point):=
-  ((X A)-(X B))^2+((Y A)-(Y B))^2 = 0.
+  ((X A)-(X B))^2%Z+((Y A)-(Y B))^2%Z = 0.
 
 Definition nequal2(A B:point):=
   (X A)<>(X B) \/ (Y A)<>(Y B).
 
 Definition nequal3(A B:point):=
-  not (((X A)-(X B))^2+((Y A)-(Y B))^2 = 0).
+  not (((X A)-(X B))^2%Z+((Y A)-(Y B))^2%Z = 0).
 
 Definition middle(A B I:point):=
-  2*(X I)=(X A)+(X B) /\ 2*(Y I)=(Y A)+(Y B).
+  2%R*(X I)=(X A)+(X B) /\ 2%R*(Y I)=(Y A)+(Y B).
 
 Definition distance2(A B:point):=
-  (X B - X A)^2 + (Y B - Y A)^2.
+  (X B - X A)^2%Z + (Y B - Y A)^2%Z.
 
 (* AB = CD *)
 Definition samedistance2(A B C D:point):=
-  (X B - X A)^2 + (Y B - Y A)^2 = (X D - X C)^2 + (Y D - Y C)^2.
+  (X B - X A)^2%Z + (Y B - Y A)^2%Z = (X D - X C)^2%Z + (Y D - Y C)^2%Z.
 Definition determinant(A O B:point):=
   (X A - X O)*(Y B - Y O) - (Y A - Y O)*(X B - X O).
 Definition scalarproduct(A O B:point):=
   (X A - X O)*(X B - X O) + (Y A - Y O)*(Y B - Y O).
 Definition norm2(A O B:point):=
-  ((X A - X O)^2+(Y A - Y O)^2)*((X B - X O)^2+(Y B - Y O)^2).
-
-
-Lemma a1:forall A B C:Prop, ((A\/B)/\(A\/C)) -> (A\/(B/\C)).
-intuition.
-Qed.
- 
-Lemma a2:forall A B C:Prop, ((A\/C)/\(B\/C)) -> ((A/\B)\/C).
-intuition.
+  ((X A - X O)^2%Z+(Y A - Y O)^2%Z)*((X B - X O)^2%Z+(Y B - Y O)^2%Z).
+
+Definition equaldistance(A B C D:point):=
+  ((X B) - (X A))^2%Z + ((Y B) - (Y A))^2%Z =
+  ((X D) - (X C))^2%Z + ((Y D) - (Y C))^2%Z.
+
+Definition equaltangente(A B C D E F:point):=
+  let s1:= determinant A B C in
+  let c1:= scalarproduct A B C in
+  let s2:= determinant D E F in
+  let c2:= scalarproduct D E F in
+  s1 * c2 = s2 * c1.
+
+Ltac cnf2 f :=
+  match f with
+   | ?A \/ (?B /\ ?C) =>
+     let c1 := cnf2 (A\/B) in
+     let c2 := cnf2 (A\/C) in constr:(c1/\c2)
+   | (?B /\ ?C) \/ ?A =>
+     let c1 := cnf2 (B\/A) in
+     let c2 := cnf2 (C\/A) in constr:(c1/\c2)
+   | (?A \/ ?B) \/ ?C =>
+     let c1 := cnf2 (B\/C) in cnf2 (A \/ c1)
+   | _ => f
+  end
+with cnf f :=
+  match f with
+   | ?A \/ ?B =>
+     let c1 := cnf A in
+       let c2 := cnf B in
+         cnf2 (c1 \/ c2)
+   | ?A /\ ?B =>
+     let c1 := cnf A in
+       let c2 := cnf B in
+         constr:(c1 /\ c2)
+   | _ => f
+  end.
+      
+Ltac scnf :=
+  match goal with
+    | |- ?f => let c := cnf f in
+      assert c;[repeat split| tauto]
+  end.
+
+Ltac disj_to_pol f :=
+  match f with
+   | ?a = ?b \/ ?g => let p := disj_to_pol g in constr:((a - b)* p)
+   | ?a = ?b => constr:(a - b)
+  end.
+
+Lemma fastnsatz1:forall x y:R, x - y = 0 -> x = y.
+nsatz.
 Qed.
 
-Lemma a3:forall a b c d:R, (a-b)*(c-d)=0 -> (a=b \/ c=d).
-intros.
-assert ( (a-b = 0) \/ (c-d = 0)).
-apply Rmult_integral.
-trivial.
-destruct H0.
-left; nsatz.
-right; nsatz.
-Qed.
+Ltac fastnsatz:=
+  try trivial; try apply fastnsatz1; try trivial; nsatz.
+  
+Ltac proof_pol_disj :=
+  match goal with
+   | |- ?g => let p := disj_to_pol g in
+     let h := fresh "hp" in
+     assert (h:p = 0);
+     [idtac|
+      prod_disj h p]
+   | _ => idtac
+  end
+with prod_disj h p :=
+  match goal with
+   | |- ?a = ?b \/ ?g => 
+        match p with
+          | ?q * ?p1 => 
+        let h0 := fresh "hp" in
+        let h1 := fresh "hp" in
+        let h2 := fresh "hp" in
+        assert (h0:a - b = 0 \/ p1 = 0);
+        [apply Rmult_integral; exact h|
+         destruct h0 as [h1|h2];
+         [left; fastnsatz|
+          right; prod_disj h2 p1]]
+        end
+   | _ => fastnsatz
+  end.
 
-Ltac geo_unfold :=
-  unfold collinear; unfold parallel; unfold notparallel; unfold orthogonal;
-  unfold equal2; unfold equal3; unfold nequal2; unfold nequal3; 
-  unfold middle; unfold samedistance2; 
-  unfold determinant; unfold scalarproduct; unfold norm2; unfold distance2.
+(*
+Goal forall a b c d e f:R, a=b \/ c=d \/ e=f \/ e=a.
+intros. scnf; proof_pol_disj .
+admit.*)
 
-Ltac geo_end :=
-  repeat (
-  repeat (match goal with h:_/\_ |- _ => decompose [and] h; clear h end);
-  repeat (apply a1 || apply a2 || apply a3);
-  repeat split).
+Ltac geo_unfold :=
+  unfold collinear, parallel, notparallel, orthogonal,
+    equal2, equal3, nequal2, nequal3,
+    middle, samedistance2,
+    determinant, scalarproduct, norm2, distance2,
+      equaltangente, determinant, scalarproduct, equaldistance.
 
 Ltac geo_rewrite_hyps:=
   repeat (match goal with
@@ -231,14 +203,41 @@ Ltac geo_rewrite_hyps:=
            | h:Y _ = _ |- _ => rewrite h in *; clear h
           end).
 
+Ltac geo_split_hyps:=
+  repeat (match goal with
+           | h:_ /\ _ |- _ => destruct h
+          end).
+
 Ltac geo_begin:=
   geo_unfold;
   intros;
   geo_rewrite_hyps;
-  geo_end.
+  geo_split_hyps;
+  scnf; proof_pol_disj.
 
 (* Examples *)
 
+Lemma medians: forall A B C A1 B1 C1 H:point,
+  middle B C A1 ->  
+  middle A C B1 -> 
+  middle A B C1 -> 
+  collinear A A1 H -> collinear B B1 H -> 
+  collinear C C1 H
+  \/ collinear A B C.
+Proof. geo_begin.
+idtac "Medians".
+ Time nsatz.
+(*Finished transaction in 2. secs (2.69359u,0.s)
+*) Qed.
+
+Lemma Pythagore: forall A B C:point,
+  orthogonal A B A C ->
+  distance2 A C + distance2 A B = distance2 B C.
+Proof. geo_begin.
+idtac "Pythagore". 
+Time nsatz.
+(*Finished transaction in 0. secs (0.354946u,0.s)
+*) Qed.
 
 Lemma Thales: forall O A B C D:point,
   collinear O A C -> collinear O B D ->
@@ -246,9 +245,268 @@ Lemma Thales: forall O A B C D:point,
   (distance2 O B * distance2 O C = distance2 O D * distance2 O A
   /\ distance2 O B * distance2 C D = distance2 O D * distance2 A B)
  \/ collinear O A B.
-repeat geo_begin.
+geo_begin.
+idtac "Thales".
+Time nsatz. (*Finished transaction in 2. secs (1.598757u,0.s)*)
+Time nsatz.
+Qed.
+
+Lemma segments_of_chords: forall A B C D M O:point,
+  equaldistance O A O B ->
+  equaldistance O A O C ->
+  equaldistance O A O D ->
+  collinear A B M ->
+  collinear C D M ->
+  (distance2 M A) * (distance2 M B) = (distance2 M C) * (distance2 M D)
+  \/ parallel A B C D.
+Proof. 
+geo_begin. 
+idtac "segments_of_chords".
+Time nsatz.
+(*Finished transaction in 3. secs (2.704589u,0.s)
+*) Qed.
+
+
+Lemma isoceles: forall A B C:point,
+  equaltangente A B C B C A ->
+  distance2 A B = distance2 A C
+  \/ collinear A B C.
+Proof. geo_begin.  Time nsatz. 
+(*Finished transaction in 1. secs (1.140827u,0.s)*) Qed.
+
+Lemma minh: forall A B C D O E H I:point,
+  X A = 0 -> Y A = 0 -> Y O = 0 ->
+  equaldistance O A O B -> 
+  equaldistance O A O C ->
+  equaldistance O A O D ->
+  orthogonal A C B D ->
+  collinear A C E ->
+  collinear B D E ->
+  collinear A B H ->
+  orthogonal E H A B ->
+  collinear C D I ->
+  middle C D I ->
+  collinear H E I
+  \/ (X C)^2%Z * (X B)^5%Z * (X O)^2%Z
+     * (X C - 2%Z * X O)^3%Z * (-2%Z * X O + X B)=0
+  \/  parallel A C B D.
+Proof. geo_begin.
+idtac "minh". 
+Time nsatz with radicalmax :=1%N strategy:=1%Z
+  parameters:=(X O::X B::X C::nil)
+  variables:= (@nil R).
+(*Finished transaction in 13. secs (10.102464u,0.s)
+*)
+Qed.
+
+Lemma Pappus: forall A B C A1 B1 C1 P Q S:point,
+  X A = 0 -> Y A = 0 -> Y B = 0 -> Y C = 0 -> 
+  collinear A1 B1 C1 ->
+  collinear A B1 P -> collinear A1 B P ->
+  collinear A C1 Q -> collinear A1 C Q ->
+  collinear B C1 S -> collinear B1 C S ->
+  collinear P Q S 
+  \/ (Y A1 - Y B1)^2%Z=0 \/ (X A = X B1)
+  \/ (X A1 = X C) \/ (X C = X B1)
+  \/ parallel A B1 A1 B \/ parallel A C1 A1 C \/ parallel B C1 B1 C.
+Proof.
+geo_begin.
+idtac "Pappus".
+Time nsatz with radicalmax :=1%N strategy:=0%Z
+  parameters:=(X B::X A1::Y A1::X B1::Y B1::X C::Y C1::nil)
+  variables:= (X B
+ :: X A1
+    :: Y A1
+       :: X B1
+          :: Y B1
+             :: X C
+                :: Y C1
+                   :: X C1 :: Y P :: X P :: Y Q :: X Q :: Y S :: X S :: nil).
+(*Finished transaction in 8. secs (7.795815u,0.000999999999999s)
+*)
+Qed.
+
+Lemma Simson: forall A B C O D E F G:point,
+  X A = 0 -> Y A = 0 -> 
+  equaldistance O A O B ->
+  equaldistance O A O C ->
+  equaldistance O A O D ->
+  orthogonal  E D B C ->
+  collinear B C E ->
+  orthogonal F D A C ->
+  collinear A C F ->
+  orthogonal G D A B ->
+  collinear A B G ->
+  collinear E F G
+  \/ (X C)^2%Z = 0 \/ (Y C)^2%Z = 0 \/ (X B)^2%Z = 0 \/ (Y B)^2%Z = 0 \/ (Y C - Y B)^2%Z = 0
+  \/ equal3 B A 
+  \/ equal3 A C \/ (X C - X B)^2%Z = 0
+  \/ equal3 B C.
+Proof.
+geo_begin.
+idtac "Simson".
+Time nsatz with radicalmax :=1%N strategy:=0%Z
+  parameters:=(X B::Y B::X C::Y C::Y D::nil)
+  variables:= (@nil R). (* compute -[X Y]. *)
+(*Finished transaction in 8. secs (7.550852u,0.s)
+*)
+Qed.
+
+Lemma threepoints: forall A B C A1 B1 A2 B2 H1 H2 H3:point,
+  (* H1 intersection of bisections *)
+  middle B C A1 ->  orthogonal H1 A1 B C ->
+  middle A C B1 -> orthogonal H1 B1 A C -> 
+  (* H2 intersection of medians *)
+  collinear A A1 H2 -> collinear B B1 H2 -> 
+  (* H3 intersection of altitudes *)
+  collinear B C A2 ->  orthogonal A A2 B C ->
+  collinear A C B2 -> orthogonal B B2 A C ->
+  collinear A A1 H3 -> collinear B B1 H3 -> 
+  collinear H1 H2 H3
+  \/ collinear A B C.
+Proof. geo_begin. 
+idtac "threepoints".
+Time nsatz. 
+(*Finished transaction in 7. secs (6.282045u,0.s)
+*) Qed.
+
+Lemma Feuerbach:  forall A B C A1 B1 C1 O A2 B2 C2 O2:point, 
+  forall r r2:R,
+  X A = 0 -> Y A =  0 -> X B = 1 -> Y B =  0->
+  middle A B C1 -> middle B C A1 -> middle C A B1 ->
+  distance2 O A1 = distance2 O B1 ->
+  distance2 O A1 = distance2 O C1 ->
+  collinear A B C2 -> orthogonal A B O2 C2 -> 
+  collinear B C A2 -> orthogonal B C O2 A2 ->
+  collinear A C B2 -> orthogonal A C O2 B2 ->
+  distance2 O2 A2 = distance2 O2 B2 ->
+  distance2 O2 A2 = distance2 O2 C2 ->
+  r^2%Z = distance2 O A1 ->
+  r2^2%Z = distance2 O2 A2 ->
+  distance2 O O2 = (r + r2)^2%Z
+  \/ distance2 O O2 = (r - r2)^2%Z
+  \/ collinear A B C.
+Proof. geo_begin. 
+idtac "Feuerbach".
+Time nsatz. 
+(*Finished transaction in 21. secs (19.021109u,0.s)*)
+Qed.
+
+
+
+
+Lemma Euler_circle: forall A B C A1 B1 C1 A2 B2 C2 O:point,
+  middle A B C1 -> middle B C A1 -> middle C A B1 ->
+  orthogonal A B C C2 -> collinear A B C2 ->
+  orthogonal B C A A2 -> collinear B C A2 ->
+  orthogonal A C B B2 -> collinear A C B2 ->
+  distance2 O A1 = distance2 O B1 ->
+  distance2 O A1 = distance2 O C1 ->
+  (distance2 O A2 = distance2 O A1
+   /\distance2 O B2 = distance2 O A1
+   /\distance2 O C2 = distance2 O A1)
+  \/ collinear A B C.
+Proof. geo_begin. 
+idtac "Euler_circle 3 goals".
+Time nsatz. 
+(*Finished transaction in 13. secs (11.208296u,0.124981s)*)
+Time nsatz.  
+(*Finished transaction in 10. secs (8.846655u,0.s)*) 
+Time nsatz. 
+(*Finished transaction in 11. secs (9.186603u,0.s)*)
+Qed.
+
+
+
+Lemma Desargues: forall A B C A1 B1 C1 P Q R S:point,
+  X S = 0 -> Y S = 0 -> Y A = 0 ->
+  collinear A S A1 -> collinear B S B1 -> collinear C S C1 ->
+  collinear B1 C1 P -> collinear B C P ->
+  collinear A1 C1 Q -> collinear A C Q -> 
+  collinear A1 B1 R -> collinear A B R ->
+  collinear P Q R
+  \/ X A = X B \/ X A = X C \/ X B = X C  \/ X A = 0 \/ Y B = 0 \/ Y C = 0
+  \/ collinear S B C \/ parallel A C A1 C1 \/ parallel A B A1 B1.
+Proof.
+geo_begin.
+idtac "Desargues".
+Time 
+let lv := rev (X A
+ :: X B
+    :: Y B
+       :: X C
+          :: Y C
+             :: Y A1 :: X A1
+                :: Y B1
+                   :: Y C1
+                      :: X R
+                         :: Y R
+                            :: X Q
+                               :: Y Q :: X P :: Y P :: X C1 :: X B1 :: nil) in
+nsatz with radicalmax :=1%N strategy:=0%Z
+  parameters:=(X A::X B::Y B::X C::Y C::X A1::Y B1::Y C1::nil)
+  variables:= lv. (*Finished transaction in 8. secs (8.02578u,0.001s)*)
+Qed.
+
+Lemma chords: forall O A B C D M:point,
+  equaldistance O A O B ->
+  equaldistance O A O C ->
+  equaldistance O A O D ->
+  collinear A B M -> collinear C D M ->
+  scalarproduct A M B = scalarproduct C M D
+  \/ parallel A B C D.
+Proof. geo_begin. 
+idtac "chords".
+ Time nsatz. 
+(*Finished transaction in 4. secs (3.959398u,0.s)*)
+Qed.
+
+Lemma Ceva: forall A B C D E F M:point,
+  collinear M A D -> collinear M B E -> collinear M C F ->
+  collinear B C D -> collinear E A C -> collinear F A B ->
+  (distance2 D B) * (distance2 E C) * (distance2 F A) =
+  (distance2 D C) * (distance2 E A) * (distance2 F B)
+  \/ collinear A B C.
+Proof. geo_begin. 
+idtac "Ceva".
 Time nsatz.
+(*Finished transaction in 105. secs (104.121171u,0.474928s)*)
+Qed.
+
+Lemma bissectrices: forall A B C M:point,
+  equaltangente C A M M A B ->
+  equaltangente A B M M B C ->
+  equaltangente B C M M C A
+  \/ equal3 A B.
+Proof. geo_begin. 
+idtac "bissectrices".
 Time nsatz.
+(*Finished transaction in 2. secs (1.937705u,0.s)*)
+Qed.
+
+Lemma bisections: forall A B C A1 B1 C1 H:point,
+  middle B C A1 ->  orthogonal H A1 B C ->
+  middle A C B1 -> orthogonal H B1 A C -> 
+  middle A B C1 -> 
+  orthogonal H C1 A B 
+  \/ collinear A B C.
+Proof. geo_begin.
+idtac "bisections". 
+Time nsatz. (*Finished transaction in 2. secs (2.024692u,0.002s)*)
+Qed.
+
+Lemma altitudes: forall A B C A1 B1 C1 H:point,
+  collinear B C A1 ->  orthogonal A A1 B C ->
+  collinear A C B1 -> orthogonal B B1 A C -> 
+  collinear A B C1 -> orthogonal C C1 A B ->
+  collinear A A1 H -> collinear B B1 H -> 
+  collinear C C1 H
+  \/ equal2 A B
+  \/ collinear A B C.
+Proof. geo_begin.
+idtac "altitudes".
+Time nsatz. (*Finished transaction in 3. secs (3.001544u,0.s)*)
+Time nsatz. (*Finished transaction in 4. secs (3.113527u,0.s)*)
 Qed.
 
 Lemma hauteurs:forall A B C A1 B1 C1 H:point,
@@ -261,26 +519,16 @@ Lemma hauteurs:forall A B C A1 B1 C1 H:point,
   \/ collinear A B C.
 
 geo_begin.
- 
-(* Time nsatzRpv 2%N 1%Z (@nil R) (@nil R).*)
-(*Finished transaction in 3. secs (2.363641u,0.s)*)
-(*Time nsatz_domainR. trop long! *)
+idtac "hauteurs".
 Time 
  let lv := constr:(Y A1
- :: X A1
-    :: Y B1
-       :: X B1
-          :: Y A0
-             :: Y B
-                :: X B
-                   :: X A0
-                      :: X H
-                         :: Y C
-                            :: Y C1 :: Y H :: X C1 :: X C :: (@Datatypes.nil R)) in
- nsatz_domainpv ltac:pretacR 2%N 1%Z (@Datatypes.nil R) lv ltac:simplR Rdi;
-  discrR.
-(* Finished transaction in 6. secs (5.579152u,0.001s) *)
+ :: X A1 :: Y B1 :: X B1 :: Y A :: Y B :: X B :: X A :: X H :: Y C
+ :: Y C1 :: Y H :: X C1 :: X C :: (@Datatypes.nil R)) in
+nsatz with radicalmax := 2%N strategy := 1%Z parameters := (@Datatypes.nil R)
+ variables := lv.
+(*Finished transaction in 5. secs (4.360337u,0.008999s)*)
 Qed.
 
+
 End Geometry.
 
diff --git a/test-suite/success/PCase.v b/test-suite/success/PCase.v
new file mode 100644
index 00000000..67d680ba
--- /dev/null
+++ b/test-suite/success/PCase.v
@@ -0,0 +1,66 @@
+
+(** Some tests of patterns containing matchs ending with joker branches.
+    Cf. the new form of the [constr_pattern] constructor [PCase]
+    in [pretyping/pattern.ml] *)
+
+(* A universal match matcher *)
+
+Ltac kill_match :=
+ match goal with
+   |- context [ match ?x with _ => _ end ] => destruct x
+ end.
+
+(* A match matcher restricted to a given type : nat *)
+
+Ltac kill_match_nat :=
+ match goal with
+   |- context [ match ?x in nat with _ => _ end ] => destruct x
+ end.
+
+(* Another way to restrict to a given type : give a branch *)
+
+Ltac kill_match_nat2 :=
+ match goal with
+   |- context [ match ?x with S _ => _ | _ => _ end ] => destruct x
+ end.
+
+(* This should act only on empty match *)
+
+Ltac kill_match_empty :=
+ match goal with
+   |- context [ match ?x with end ] => destruct x
+ end.
+
+Lemma test1 (b:bool) : if b then True else O=O.
+Proof.
+ Fail kill_match_nat.
+ Fail kill_match_nat2.
+ Fail kill_match_empty.
+ kill_match. exact I. exact eq_refl.
+Qed.
+
+Lemma test2a (n:nat) : match n with O => True | S n => (n = n) end.
+Proof.
+ Fail kill_match_empty.
+ kill_match_nat. exact I. exact eq_refl.
+Qed.
+
+Lemma test2b (n:nat) : match n with O => True | S n => (n = n) end.
+Proof.
+ kill_match_nat2. exact I. exact eq_refl.
+Qed.
+
+Lemma test2c (n:nat) : match n with O => True | S n => (n = n) end.
+Proof.
+ kill_match. exact I. exact eq_refl.
+Qed.
+
+Lemma test3a (f:False) : match f return Prop with end.
+Proof.
+ kill_match_empty.
+Qed.
+
+Lemma test3b (f:False) : match f return Prop with end.
+Proof.
+ kill_match.
+Qed.
diff --git a/test-suite/success/PrintSortedUniverses.v b/test-suite/success/PrintSortedUniverses.v
new file mode 100644
index 00000000..81326580
--- /dev/null
+++ b/test-suite/success/PrintSortedUniverses.v
@@ -0,0 +1,2 @@
+Require Reals.
+Print Sorted Universes.
diff --git a/test-suite/success/ProgramWf.v b/test-suite/success/ProgramWf.v
index 81bdbc29..00a13aed 100644
--- a/test-suite/success/ProgramWf.v
+++ b/test-suite/success/ProgramWf.v
@@ -1,3 +1,9 @@
+(* Before loading Program, check non-anomaly on missing library Program *)
+
+Fail Program Definition f n (e:n=n): {n|n=0} := match n,e with 0, refl => 0 | _, _ => 0 end.
+
+(* Then we test Program properly speaking *)
+
 Require Import Arith Program.
 Require Import ZArith Zwf.
 
diff --git a/test-suite/success/RecTutorial.v b/test-suite/success/RecTutorial.v
index d4e6a82e..2602c7e3 100644
--- a/test-suite/success/RecTutorial.v
+++ b/test-suite/success/RecTutorial.v
@@ -55,13 +55,13 @@ Check (cons 3 (cons 2 nil)).
 
 Require Import Bvector.
 
-Print vector.
+Print Vector.t.
 
-Check (Vnil nat).
+Check (Vector.nil nat).
 
-Check (fun (A:Set)(a:A)=> Vcons _ a _ (Vnil _)).
+Check (fun (A:Set)(a:A)=> Vector.cons _ a _ (Vector.nil _)).
 
-Check (Vcons _ 5 _ (Vcons _ 3 _ (Vnil _))).
+Check (Vector.cons _ 5 _ (Vector.cons _ 3 _ (Vector.nil _))).
 
 
 
@@ -315,16 +315,16 @@ Proof.
 Qed.
 
 Definition Vtail_total
-   (A : Set) (n : nat) (v : vector A n) : vector A (pred n):=
-match v in (vector _ n0) return (vector A (pred n0)) with
-| Vnil => Vnil A
-| Vcons _ n0 v0 => v0
+   (A : Set) (n : nat) (v : Vector.t A n) : Vector.t A (pred n):=
+match v in (Vector.t _ n0) return (Vector.t A (pred n0)) with
+| Vector.nil => Vector.nil A
+| Vector.cons _ n0 v0 => v0
 end.
 
-Definition Vtail' (A:Set)(n:nat)(v:vector A n) : vector A (pred n).
+Definition Vtail' (A:Set)(n:nat)(v:Vector.t A n) : Vector.t A (pred n).
  case v.
  simpl.
- exact (Vnil A).
+ exact (Vector.nil A).
  simpl.
  auto.
 Defined.
@@ -543,7 +543,7 @@ Inductive ex_Set  (P : Set -> Prop) : Type :=
 Inductive comes_from_the_left (P Q:Prop): P \/ Q -> Prop :=
   c1 : forall p, comes_from_the_left P Q (or_introl (A:=P) Q p).
 
-Goal (comes_from_the_left _ _ (or_introl  True I)).
+Goal (comes_from_the_left _ _ (or_introl True I)).
 split.
 Qed.
 
@@ -966,37 +966,37 @@ let rec div_aux x y =
            | Right -> div_aux (minus x y) y)
 *)
 
-Lemma vector0_is_vnil : forall (A:Set)(v:vector A 0), v = Vnil A.
+Lemma vector0_is_vnil : forall (A:Set)(v:Vector.t A 0), v = Vector.nil A.
 Proof.
  intros A v;inversion v.
 Abort.
 
 (*
- Lemma vector0_is_vnil_aux : forall (A:Set)(n:nat)(v:vector A n),
+ Lemma Vector.t0_is_vnil_aux : forall (A:Set)(n:nat)(v:Vector.t A n),
                                   n= 0 -> v = Vnil A.
 
 Toplevel input, characters 40281-40287
-> Lemma vector0_is_vnil_aux : forall (A:Set)(n:nat)(v:vector A n),                                    n= 0 -> v = Vnil A.
+> Lemma Vector.t0_is_vnil_aux : forall (A:Set)(n:nat)(v:Vector.t A n),                                    n= 0 -> v = Vnil A.
 >                                                                                                                 ^^^^^^
 Error: In environment
 A : Set
 n : nat
-v : vector A n
+v : Vector.t A n
 e : n = 0
-The term "Vnil A" has type "vector A 0" while it is expected to have type
- "vector A n"
+The term "Vnil A" has type "Vector.t A 0" while it is expected to have type
+ "Vector.t A n"
 *)
  Require Import JMeq.
 
-Lemma vector0_is_vnil_aux : forall (A:Set)(n:nat)(v:vector A n),
-                                  n= 0 -> JMeq v (Vnil A).
+Lemma vector0_is_vnil_aux : forall (A:Set)(n:nat)(v:Vector.t A n),
+                                  n= 0 -> JMeq v (Vector.nil A).
 Proof.
  destruct v.
  auto.
  intro; discriminate.
 Qed.
 
-Lemma vector0_is_vnil : forall (A:Set)(v:vector A 0), v = Vnil A.
+Lemma vector0_is_vnil : forall (A:Set)(v:Vector.t A 0), v = Vector.nil A.
 Proof.
  intros a v;apply JMeq_eq.
  apply vector0_is_vnil_aux.
@@ -1004,56 +1004,56 @@ Proof.
 Qed.
 
 
-Implicit Arguments Vcons [A n].
-Implicit Arguments Vnil [A].
-Implicit Arguments Vhead [A n].
-Implicit Arguments Vtail [A n].
+Implicit Arguments Vector.cons [A n].
+Implicit Arguments Vector.nil [A].
+Implicit Arguments Vector.hd [A n].
+Implicit Arguments Vector.tl [A n].
 
-Definition Vid : forall (A : Type)(n:nat), vector A n -> vector A n.
+Definition Vid : forall (A : Type)(n:nat), Vector.t A n -> Vector.t A n.
 Proof.
  destruct n; intro v.
- exact Vnil.
- exact (Vcons  (Vhead v) (Vtail v)).
+ exact Vector.nil.
+ exact (Vector.cons  (Vector.hd v) (Vector.tl v)).
 Defined.
 
-Eval simpl in (fun (A:Set)(v:vector A 0) => (Vid _ _ v)).
+Eval simpl in (fun (A:Set)(v:Vector.t A 0) => (Vid _ _ v)).
 
-Eval simpl in (fun (A:Set)(v:vector A 0) => v).
+Eval simpl in (fun (A:Set)(v:Vector.t A 0) => v).
 
 
 
-Lemma Vid_eq : forall (n:nat) (A:Type)(v:vector A n), v=(Vid _ n v).
+Lemma Vid_eq : forall (n:nat) (A:Type)(v:Vector.t A n), v=(Vid _ n v).
 Proof.
  destruct v.
  reflexivity.
  reflexivity.
 Defined.
 
-Theorem zero_nil : forall A (v:vector A 0), v = Vnil.
+Theorem zero_nil : forall A (v:Vector.t A 0), v = Vector.nil.
 Proof.
  intros.
- change (Vnil (A:=A)) with (Vid _ 0 v).
+ change (Vector.nil (A:=A)) with (Vid _ 0 v).
  apply Vid_eq.
 Defined.
 
 
 Theorem decomp :
-  forall (A : Set) (n : nat) (v : vector A (S n)),
-  v = Vcons (Vhead v) (Vtail v).
+  forall (A : Set) (n : nat) (v : Vector.t A (S n)),
+  v = Vector.cons (Vector.hd v) (Vector.tl v).
 Proof.
  intros.
- change (Vcons (Vhead v) (Vtail v)) with (Vid _  (S n) v).
+ change (Vector.cons (Vector.hd v) (Vector.tl v)) with (Vid _  (S n) v).
  apply Vid_eq.
 Defined.
 
 
 
 Definition vector_double_rect :
-    forall (A:Set) (P: forall (n:nat),(vector A n)->(vector A n) -> Type),
-        P 0 Vnil Vnil ->
-        (forall n (v1 v2 : vector A n) a b, P n v1 v2 ->
-             P (S n) (Vcons a v1) (Vcons  b v2)) ->
-        forall n (v1 v2 : vector A n), P n v1 v2.
+    forall (A:Set) (P: forall (n:nat),(Vector.t A n)->(Vector.t A n) -> Type),
+        P 0 Vector.nil Vector.nil ->
+        (forall n (v1 v2 : Vector.t A n) a b, P n v1 v2 ->
+             P (S n) (Vector.cons a v1) (Vector.cons  b v2)) ->
+        forall n (v1 v2 : Vector.t A n), P n v1 v2.
  induction n.
  intros; rewrite (zero_nil _ v1); rewrite (zero_nil _ v2).
  auto.
@@ -1063,24 +1063,24 @@ Defined.
 
 Require Import Bool.
 
-Definition bitwise_or n v1 v2 : vector bool n :=
-   vector_double_rect bool  (fun n v1 v2 => vector bool n)
-                        Vnil
-                        (fun n v1 v2 a b r => Vcons (orb a b) r) n v1 v2.
+Definition bitwise_or n v1 v2 : Vector.t bool n :=
+   vector_double_rect bool  (fun n v1 v2 => Vector.t bool n)
+                        Vector.nil
+                        (fun n v1 v2 a b r => Vector.cons (orb a b) r) n v1 v2.
 
 
-Fixpoint vector_nth (A:Set)(n:nat)(p:nat)(v:vector A p){struct v}
+Fixpoint vector_nth (A:Set)(n:nat)(p:nat)(v:Vector.t A p){struct v}
                   : option A :=
   match n,v  with
-    _   , Vnil => None
-  | 0   , Vcons b  _ _ => Some b
-  | S n', Vcons _  p' v' => vector_nth A n'  p' v'
+    _   , Vector.nil => None
+  | 0   , Vector.cons b  _ _ => Some b
+  | S n', Vector.cons _  p' v' => vector_nth A n'  p' v'
   end.
 
 Implicit Arguments vector_nth [A p].
 
 
-Lemma nth_bitwise : forall (n:nat) (v1 v2: vector bool n) i  a b,
+Lemma nth_bitwise : forall (n:nat) (v1 v2: Vector.t bool n) i  a b,
       vector_nth i v1 = Some a ->
       vector_nth i v2 = Some b ->
       vector_nth i (bitwise_or _ v1 v2) = Some (orb a b).
diff --git a/test-suite/success/Scheme.v b/test-suite/success/Scheme.v
new file mode 100644
index 00000000..dd5aa81d
--- /dev/null
+++ b/test-suite/success/Scheme.v
@@ -0,0 +1,4 @@
+(* This failed in 8.3pl2 *)
+
+Scheme Induction for eq Sort Prop.
+Check eq_ind_dep.
diff --git a/test-suite/success/Tauto.v b/test-suite/success/Tauto.v
index 324d340a..c4e67677 100644
--- a/test-suite/success/Tauto.v
+++ b/test-suite/success/Tauto.v
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: Tauto.v 14641 2011-11-06 11:59:10Z herbelin $ *)
-
 (**** Tactics Tauto and Intuition ****)
 
 (**** Tauto:
diff --git a/test-suite/success/TestRefine.v b/test-suite/success/TestRefine.v
index 6cc443bb..705bdc45 100644
--- a/test-suite/success/TestRefine.v
+++ b/test-suite/success/TestRefine.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/test-suite/success/apply.v b/test-suite/success/apply.v
index a6f9fa23..e3183ef2 100644
--- a/test-suite/success/apply.v
+++ b/test-suite/success/apply.v
@@ -202,6 +202,13 @@ try apply H.
 unfold ID; apply H0.
 Qed.
 
+(* Test hyp in "apply -> ... in hyp" is correctly instantiated by Ltac *)
+
+Goal (True <-> False) -> True -> False.
+intros Heq H.
+match goal with [ H : True |- _ ] => apply -> Heq in H end.
+Abort.
+
 (* Test coercion below product and on non meta-free terms in with bindings *)
 (* Cf wishes #1408 from E. Makarov *)
 
@@ -326,13 +333,12 @@ exact (refl_equal 4).
 Qed.
 
 (* From 12612, descent in conjunctions is more powerful *)
-(* The following, which was failing badly in bug 1980, is now accepted
-   (even if somehow surprising) *)
+(* The following, which was failing badly in bug 1980, is now
+   properly rejected, as descend in conjunctions builds an
+   ill-formed elimination from Prop to Type. *)
 
 Goal True.
-eapply ex_intro.
-instantiate (2:=fun _ :True => True).
-instantiate (1:=I).
+Fail eapply ex_intro.
 exact I.
 Qed.
 
@@ -391,3 +397,21 @@ intro x;
 apply x.
 
 *)
+
+Section A.
+
+Variable map : forall (T1 T2 : Type) (f : T1 -> T2) (t11 t12 : T1),
+  identity (f t11) (f t12).
+
+Variable mapfuncomp : forall (X Y Z : Type) (f : X -> Y) (g : Y -> Z) (x x' : X),
+  identity (map Y Z g (f x) (f x')) (map X Z (fun x0 : X => g (f x0)) x x').
+
+Goal forall X:Type, forall Y:Type, forall f:X->Y, forall x : X, forall x' : X, 
+  forall g : Y -> X,
+  let gf := (fun x : X => g (f x)) : X -> X in
+   identity (map Y X g (f x) (f x')) (map X X gf x x').
+intros.
+apply mapfuncomp.
+Abort.
+
+End A.
diff --git a/test-suite/success/auto.v b/test-suite/success/auto.v
new file mode 100644
index 00000000..9b691e25
--- /dev/null
+++ b/test-suite/success/auto.v
@@ -0,0 +1,26 @@
+(* Wish #2154 by E. van der Weegen *)
+
+(* auto was not using f_equal-style lemmas with metavariables occuring
+   only in the type of an evar of the concl, but not directly in the
+   concl itself *)
+
+Parameters
+  (F: Prop -> Prop)
+  (G: forall T, (T -> Prop) -> Type)
+  (L: forall A (P: A -> Prop), G A P -> forall x, F (P x))
+  (Q: unit -> Prop).
+
+Hint Resolve L.
+
+Goal G unit Q -> F (Q tt).
+  intro.
+  auto.
+Qed.
+
+(* Test implicit arguments in "using" clause *)
+
+Goal forall n:nat, nat * nat.
+auto using (pair O).
+Undo.
+eauto using (pair O).
+Qed.
diff --git a/test-suite/success/autorewritein.v b/test-suite/success/autorewrite.v
index 68f2f7ce..5e9064f8 100644
--- a/test-suite/success/autorewritein.v
+++ b/test-suite/success/autorewrite.v
@@ -19,5 +19,11 @@ Proof.
     apply H;reflexivity.
 Qed.
 
+(* Check autorewrite does not solve existing evars *)
+(* See discussion started by A. Chargueraud in Oct 2010 on coqdev *)
 
+Hint Rewrite <- plus_n_O : base1.
+Goal forall y, exists x, y+x = y.
+eexists. autorewrite with base1.
+Fail reflexivity.
 
diff --git a/test-suite/success/bullet.v b/test-suite/success/bullet.v
new file mode 100644
index 00000000..1099f3e1
--- /dev/null
+++ b/test-suite/success/bullet.v
@@ -0,0 +1,5 @@
+Goal True /\ True.
+split.
+- exact I.
+- exact I.
+Qed.
diff --git a/test-suite/success/change.v b/test-suite/success/change.v
index 5ac6ce82..c65cf303 100644
--- a/test-suite/success/change.v
+++ b/test-suite/success/change.v
@@ -30,3 +30,11 @@ change 3 at 1 with (1+2) in H |- *.
 change 3 at 1 with (1+2) in H, H|-.
 change 3 in |- * at 1.
  *)
+
+(* Test that pretyping checks allowed elimination sorts *)
+
+Goal True.
+Fail change True with (let (x,a) := ex_intro _ True (eq_refl True) in x).
+Fail change True with
+        match ex_intro _ True (eq_refl True) with ex_intro x _ => x end.
+Abort.
diff --git a/test-suite/success/coercions.v b/test-suite/success/coercions.v
index 908b5f77..001beae7 100644
--- a/test-suite/success/coercions.v
+++ b/test-suite/success/coercions.v
@@ -81,3 +81,11 @@ Coercion irrelevent := (fun _ => I) : True -> car (Build_Setoid True).
 
 Definition ClaimB := forall (X Y:Setoid) (f: extSetoid X Y) (x:X), f x= f x.
 
+(* Check that coercions are made visible only when modules are imported *)
+
+Module A.
+  Module B. Coercion b2n (b:bool) := if b then 0 else 1. End B.
+  Fail Check S true.
+End A.
+Import A.
+Fail Check S true.
diff --git a/test-suite/success/conv_pbs.v b/test-suite/success/conv_pbs.v
index f6ebacae..05d2c98f 100644
--- a/test-suite/success/conv_pbs.v
+++ b/test-suite/success/conv_pbs.v
@@ -221,3 +221,8 @@ with universal_completeness_stoup (Gamma:context)(A:formula){struct A}
           (ProofForallL x t (subst_formula (remove_assoc _ x rho) A)
           (eq_rect _ (fun D => Gamma'' ; D |- C) p _ (subst_commute _ _ _ _)))))
   end.
+
+
+(* A simple example that raised an uncaught exception at some point *)
+
+Fail Check fun x => @eq_refl x <: true = true.
diff --git a/test-suite/success/destruct.v b/test-suite/success/destruct.v
index 8013e1d3..fc40ea96 100644
--- a/test-suite/success/destruct.v
+++ b/test-suite/success/destruct.v
@@ -74,3 +74,22 @@ destruct H.
 destruct H0.
 reflexivity.
 Qed.
+
+(* These did not work before 8.4 *)
+
+Goal (exists x, x=0) -> True.
+destruct 1 as (_,_); exact I.
+Abort.
+
+Goal (exists x, x=0 /\ True) -> True.
+destruct 1 as (_,(_,H)); exact H.
+Abort.
+
+Goal (exists x, x=0 /\ True) -> True.
+destruct 1 as (_,(_,x)); exact x.
+Abort.
+
+Goal let T:=nat in forall (x:nat) (g:T -> nat), g x = 0.
+intros.
+destruct (g _). (* This was failing in at least r14571 *)
+Abort.
diff --git a/test-suite/success/eauto.v b/test-suite/success/eauto.v
index 1862ad10..a94d8b1d 100644
--- a/test-suite/success/eauto.v
+++ b/test-suite/success/eauto.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/test-suite/success/eqdecide.v b/test-suite/success/eqdecide.v
index ff880d00..8c00583e 100644
--- a/test-suite/success/eqdecide.v
+++ b/test-suite/success/eqdecide.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -16,12 +16,7 @@ Qed.
 
 Lemma lem2 : forall x y : T, {x = y} + {x <> y}.
 intros x y.
- decide equality x y.
-Qed.
-
-Lemma lem3 : forall x y : T, {x = y} + {x <> y}.
-intros x y.
- decide equality y x.
+ decide equality.
 Qed.
 
 Lemma lem4 : forall x y : T, {x = y} + {x <> y}.
diff --git a/test-suite/success/eta.v b/test-suite/success/eta.v
new file mode 100644
index 00000000..08078012
--- /dev/null
+++ b/test-suite/success/eta.v
@@ -0,0 +1,19 @@
+(* Kernel test (head term is a constant) *)
+Check (fun a : S = S => a : S = fun x => S x).
+
+(* Kernel test (head term is a variable) *)
+Check (fun (f:nat->nat) (a : f = f) => a : f = fun x => f x).
+
+(* Test type inference  (head term is syntactically rigid) *)
+Check (fun (a : list = list) => a : list = fun A => _ A).
+
+(* Test type inference (head term is a variable) *)
+(* This one is still to be done...
+Check (fun (f:nat->nat) (a : f = f) => a : f = fun x => _ x).
+*)
+
+(* Test tactic unification *)
+Goal (forall f:nat->nat, (fun x => f x) = (fun x => f x)) -> S = S.
+intro H; apply H.
+Qed.
+
diff --git a/test-suite/success/evars.v b/test-suite/success/evars.v
index 6423ad14..2f1ec757 100644
--- a/test-suite/success/evars.v
+++ b/test-suite/success/evars.v
@@ -238,3 +238,74 @@ eapply f_equal with (* should fail because ill-typed *)
         end) in H
 || injection H.
 Abort.
+
+(* A legitimate simple eapply that was failing in coq <= 8.3.
+   Cf. in Unification.w_merge the addition of an extra pose_all_metas_as_evars
+   on 30/9/2010
+*)
+
+Lemma simple_eapply_was_failing :
+ (forall f:nat->nat, exists g, f = g) -> True.
+Proof.
+ assert (modusponens : forall P Q, P -> (P->Q) -> Q) by auto.
+ intros.
+ eapply modusponens.
+ simple eapply H.
+ (* error message with V8.3 :
+    Impossible to unify "?18" with "fun g : nat -> nat => ?6 = g". *)
+Abort.
+
+(* Regression test *)
+
+Definition fo : option nat -> nat := option_rec _ (fun a => 0) 0.
+
+(* This example revealed an incorrect evar restriction at some time
+   around October 2011 *)
+
+Goal forall (A:Type) (a:A) (P:forall A, A -> Prop), (P A a) /\ (P A a).
+intros.
+refine ((fun H => conj (proj1 H) (proj2 H)) _).
+Abort.
+
+(* The argument of e below failed to be inferred from r14219 (Oct 2011) to *)
+(* r14753 after the restrictions made on detecting Miller's pattern in the *)
+(* presence of alias, only the second-order unification procedure was *)
+(* able to solve this problem but it was deactivated for 8.4 in r14219 *)
+
+Definition k0
+  (e:forall P : nat -> Prop, (exists n : nat, P n) -> nat)
+  (j : forall a, exists n : nat, n = a) o :=
+ match o with (* note: match introduces an alias! *)
+ | Some a => e _ (j a)
+ | None => O
+ end.
+
+Definition k1
+  (e:forall P : nat -> Prop, (exists n : nat, P n) -> nat)
+  (j : forall a, exists n : nat, n = a) a (b:=a) := e _ (j a).
+
+Definition k2
+  (e:forall P : nat -> Prop, (exists n : nat, P n) -> nat)
+  (j : forall a, exists n : nat, n = a) a (b:=a) := e _ (j b).
+
+(* Other examples about aliases involved in pattern unification *)
+
+Definition k3
+  (e:forall P : nat -> Prop, (exists n : nat, P n) -> nat)
+  (j : forall a, exists n : nat, let a' := a in n = a') a (b:=a) := e _ (j b).
+
+Definition k4
+  (e:forall P : nat -> Prop, (exists n : nat, P n) -> nat)
+  (j : forall a, exists n : nat, let a' := S a in n = a') a (b:=a) := e _ (j b).
+
+Definition k5
+  (e:forall P : nat -> Prop, (exists n : nat, P n) -> nat)
+  (j : forall a, let a' := S a in exists n : nat, n = a') a (b:=a) := e _ (j b).
+
+Definition k6
+  (e:forall P : nat -> Prop, (exists n : nat, P n) -> nat)
+  (j : forall a, exists n : nat, let n' := S n in n' = a) a (b:=a) := e _ (j b).
+
+Definition k7
+  (e:forall P : nat -> Prop, (exists n : nat, let n' := n in P n') -> nat)
+  (j : forall a, exists n : nat, n = a) a (b:=a) := e _ (j b).
diff --git a/test-suite/success/extraction.v b/test-suite/success/extraction.v
index 4fec6e7f..3f8a3bc4 100644
--- a/test-suite/success/extraction.v
+++ b/test-suite/success/extraction.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -342,7 +342,7 @@ case H1.
 exact H0.
 intros.
 exact n.
-Qed.
+Defined.
 Extraction oups.
 (*
 let oups h0 =
diff --git a/test-suite/success/fix.v b/test-suite/success/fix.v
index be4e0684..b25b502c 100644
--- a/test-suite/success/fix.v
+++ b/test-suite/success/fix.v
@@ -9,13 +9,12 @@ Inductive rBoolOp : Set :=
   | rAnd : rBoolOp
   | rEq : rBoolOp.
 
-Definition rlt (a b : rNat) : Prop :=
-  (a ?= b)%positive Datatypes.Eq = Datatypes.Lt.
+Definition rlt (a b : rNat) : Prop := Pcompare a b Eq = Lt.
 
 Definition rltDec : forall m n : rNat, {rlt m n} + {rlt n m \/ m = n}.
 intros n m; generalize (nat_of_P_lt_Lt_compare_morphism n m);
  generalize (nat_of_P_gt_Gt_compare_morphism n m);
- generalize (Pcompare_Eq_eq n m); case ((n ?= m)%positive Datatypes.Eq).
+ generalize (Pcompare_Eq_eq n m); case (Pcompare n m Eq).
 intros H' H'0 H'1; right; right; auto.
 intros H' H'0 H'1; left; unfold rlt in |- *.
 apply nat_of_P_lt_Lt_compare_complement_morphism; auto.
diff --git a/test-suite/success/implicit.v b/test-suite/success/implicit.v
index ce3e692f..e8019a90 100644
--- a/test-suite/success/implicit.v
+++ b/test-suite/success/implicit.v
@@ -107,3 +107,20 @@ Context {A:Set}.
 Definition h (a:A) := a.
 End C.
 Check h 0.
+
+(* Check implicit arguments in arity of inductive types. The three
+   following examples used to fail before r13671 *)
+
+Inductive I {A} (a:A) : forall {n:nat}, Prop :=
+ | C : I a (n:=0).
+
+Inductive I2 (x:=0) : Prop :=
+ | C2 {p:nat} : p = 0 -> I2.
+Check C2 eq_refl.
+
+Inductive I3 {A} (x:=0) (a:A) : forall {n:nat}, Prop :=
+ | C3 : I3 a (n:=0).
+
+(* Check global implicit declaration over ref not in section *)
+
+Section D. Global Arguments eq [A] _ _. End D.
diff --git a/test-suite/success/inds_type_sec.v b/test-suite/success/inds_type_sec.v
index 7626ecc4..234c4223 100644
--- a/test-suite/success/inds_type_sec.v
+++ b/test-suite/success/inds_type_sec.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/test-suite/success/induct.v b/test-suite/success/induct.v
index 3c8d8ea9..b24ed2f1 100644
--- a/test-suite/success/induct.v
+++ b/test-suite/success/induct.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -41,3 +41,26 @@ Proof.
   auto.
   auto.
 Qed.
+
+(* Check selection of occurrences by pattern *)
+
+Goal forall x, S x = S (S x).   
+intros.
+induction (S _) in |- * at -2.
+now_show (0=1).
+Undo 2.
+induction (S _) in |- * at 1 3.
+now_show (0=1).
+Undo 2.
+induction (S _) in |- * at 1.
+now_show (0=S (S x)).
+Undo 2.
+induction (S _) in |- * at 2.
+now_show (S x=0).
+Undo 2.
+induction (S _) in |- * at 3.
+now_show (S x=1).
+Undo 2.
+Fail induction (S _) in |- * at 4.
+Abort.
+
diff --git a/test-suite/success/ltac.v b/test-suite/success/ltac.v
index 02618c2c..7387add6 100644
--- a/test-suite/success/ltac.v
+++ b/test-suite/success/ltac.v
@@ -244,6 +244,29 @@ reflexivity.
 apply I.
 Qed.
 
+(* Test binding of open terms with non linear matching *)
+
+Ltac f_non_linear t :=
+  match t with
+    (forall x y, ?u = 0) -> (forall y x, ?u = 0) =>
+       assert (forall x y:nat, u = u)
+  end.
+
+Goal True.
+f_non_linear ((forall x y, x+y = 0) -> (forall x y, y+x = 0)).
+reflexivity.
+f_non_linear ((forall a b, a+b = 0) -> (forall a b, b+a = 0)).
+reflexivity.
+f_non_linear ((forall a b, a+b = 0) -> (forall x y, y+x = 0)).
+reflexivity.
+f_non_linear ((forall x y, x+y = 0) -> (forall a b, b+a = 0)).
+reflexivity.
+f_non_linear ((forall x y, x+y = 0) -> (forall y x, x+y = 0)).
+reflexivity.
+f_non_linear ((forall x y, x+y = 0) -> (forall y x, y+x = 0)) (* should fail *)
+|| exact I.
+Qed.
+
 (* Test regular failure when clear/intro breaks soundness of the
    interpretation of terms in current environment *)
 
@@ -275,3 +298,7 @@ evar(foo:nat).
 let evval := eval compute in foo in not_eq evval 1.
 let evval := eval compute in foo in not_eq 1 evval.
 Abort.
+
+(* Check that this returns an error and not an anomaly (see r13667) *)
+
+Fail Local Tactic Notation "myintro" := intro.
diff --git a/test-suite/success/mutual_ind.v b/test-suite/success/mutual_ind.v
index 41aa3b3e..fcadd150 100644
--- a/test-suite/success/mutual_ind.v
+++ b/test-suite/success/mutual_ind.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/test-suite/success/polymorphism.v b/test-suite/success/polymorphism.v
index 5a008f18..56cab0f6 100644
--- a/test-suite/success/polymorphism.v
+++ b/test-suite/success/polymorphism.v
@@ -9,4 +9,4 @@ End S.
 (*
 Check f nat nat : Set.
 *)
-Check I nat nat : Set.
+Check I nat nat : Set.
+\ No newline at end of file
diff --git a/test-suite/success/proof_using.v b/test-suite/success/proof_using.v
new file mode 100644
index 00000000..93a9ef11
--- /dev/null
+++ b/test-suite/success/proof_using.v
@@ -0,0 +1,61 @@
+Section Foo.
+
+Variable a : nat.
+
+Lemma l1 : True.
+Fail Proof using non_existing.
+Proof using a.
+exact I.
+Qed.
+
+Lemma l2 : True.
+Proof using a.
+Admitted.
+
+Lemma l3 : True.
+Proof using a.
+admit.
+Qed.
+
+End Foo.
+
+Check (l1 3).
+Check (l2 3).
+Check (l3 3).
+
+Section Bar.
+
+Variable T : Type.
+Variable a b : T.
+Variable H : a = b.
+
+Lemma l4 : a = b.
+Proof using H.
+exact H.
+Qed.
+
+End Bar.
+
+Check (l4 _ 1 1 _ : 1 = 1).
+
+Section S1.
+
+Variable v1 : nat.
+
+Section S2.
+
+Variable v2 : nat.
+
+Lemma deep : v1 = v2.
+Proof using v1 v2.
+admit.
+Qed.
+
+End S2.
+
+Check (deep 3 : v1 = 3).
+
+End S1.
+
+Check (deep 3 4 : 3 = 4).
+
diff --git a/test-suite/success/remember.v b/test-suite/success/remember.v
new file mode 100644
index 00000000..3241e133
--- /dev/null
+++ b/test-suite/success/remember.v
@@ -0,0 +1,8 @@
+(* Testing remember and co *)
+
+Lemma A : forall (P: forall X, X -> Prop), P nat 0 -> P nat 0.
+intros.
+Fail remember nat as X.
+Fail remember nat as X in H. (* This line used to succeed in 8.3 *)
+Fail remember nat as X in |- *.
+Abort.
diff --git a/test-suite/success/rewrite.v b/test-suite/success/rewrite.v
index 3bce52fe..08c406be 100644
--- a/test-suite/success/rewrite.v
+++ b/test-suite/success/rewrite.v
@@ -108,3 +108,24 @@ intros.
 rewrite (H _).
 reflexivity.
 Qed.
+
+(* Example of rewriting of a degenerated pattern using the right-most
+   argument of the goal. This is sometimes used in contribs, even if
+   ad hoc. Here, we have the extra requirement that checking types
+   needs delta-conversion *)
+
+Axiom s : forall (A B : Type) (p : A * B), p = (fst p, snd p).
+Definition P := (nat * nat)%type.
+Goal forall x:P, x = x.
+intros. rewrite s.
+Abort.
+
+(* Test second-order unification and failure of pattern-unification *)
+
+Goal forall (P: forall Y, Y -> Prop) Y a, Y = nat -> (True -> P Y a) -> False.
+intros.
+(* The next line used to succeed between June and November 2011 *)
+(* causing ill-typed rewriting *)
+Fail rewrite H in H0.
+Abort.
+
diff --git a/test-suite/success/searchabout.v b/test-suite/success/searchabout.v
new file mode 100644
index 00000000..d9ade314
--- /dev/null
+++ b/test-suite/success/searchabout.v
@@ -0,0 +1,60 @@
+
+(** Test of the different syntaxes of SearchAbout, in particular
+    with and without the [ ... ] delimiters *)
+
+SearchAbout plus.
+SearchAbout plus mult.
+SearchAbout "plus_n".
+SearchAbout plus "plus_n".
+SearchAbout "*".
+SearchAbout "*" "+".
+
+SearchAbout plus inside Peano.
+SearchAbout plus mult inside Peano.
+SearchAbout "plus_n" inside Peano.
+SearchAbout plus "plus_n" inside Peano.
+SearchAbout "*" inside Peano.
+SearchAbout "*" "+" inside Peano.
+
+SearchAbout plus outside Peano Logic.
+SearchAbout plus mult outside Peano Logic.
+SearchAbout "plus_n" outside Peano Logic.
+SearchAbout plus "plus_n" outside Peano Logic.
+SearchAbout "*" outside Peano Logic.
+SearchAbout "*" "+" outside Peano Logic.
+
+SearchAbout -"*" "+" outside Logic.
+SearchAbout -"*"%nat "+"%nat outside Logic.
+
+SearchAbout [plus].
+SearchAbout [plus mult].
+SearchAbout ["plus_n"].
+SearchAbout [plus "plus_n"].
+SearchAbout ["*"].
+SearchAbout ["*" "+"].
+
+SearchAbout [plus] inside Peano.
+SearchAbout [plus mult] inside Peano.
+SearchAbout ["plus_n"] inside Peano.
+SearchAbout [plus "plus_n"] inside Peano.
+SearchAbout ["*"] inside Peano.
+SearchAbout ["*" "+"] inside Peano.
+
+SearchAbout [plus] outside Peano Logic.
+SearchAbout [plus mult] outside Peano Logic.
+SearchAbout ["plus_n"] outside Peano Logic.
+SearchAbout [plus "plus_n"] outside Peano Logic.
+SearchAbout ["*"] outside Peano Logic.
+SearchAbout ["*" "+"] outside Peano Logic.
+
+SearchAbout [-"*" "+"] outside Logic.
+SearchAbout [-"*"%nat "+"%nat] outside Logic.
+
+
+(** The example in the Reference Manual *)
+
+Require Import ZArith.
+
+SearchAbout Zmult Zplus "distr".
+SearchAbout "+"%Z "*"%Z "distr" -positive -Prop.
+SearchAbout (?x * _ + ?x * _)%Z outside OmegaLemmas.
diff --git a/test-suite/success/setoid_test.v b/test-suite/success/setoid_test.v
index 033b3f48..19693d70 100644
--- a/test-suite/success/setoid_test.v
+++ b/test-suite/success/setoid_test.v
@@ -130,3 +130,38 @@ intros f0 Q H.
 setoid_rewrite H.
 tauto.
 Qed.
+
+(** Check proper refreshing of the lemma application for multiple 
+   different instances in a single setoid rewrite. *)
+
+Section mult.
+  Context (fold : forall {A} {B}, (A -> B) -> A -> B).
+  Context (add : forall A, A -> A).
+  Context (fold_lemma : forall {A B f} {eqA : relation B} x, eqA (fold A B f (add A x)) (fold _ _ f x)).
+  Context (ab : forall B, A -> B).
+  Context (anat : forall A, nat -> A).
+
+Goal forall x, (fold _ _ (fun x => ab A x) (add A x) = anat _ (fold _ _ (ab nat) (add _ x))). 
+Proof. intros.
+  setoid_rewrite fold_lemma. 
+  change (fold A A (fun x0 : A => ab A x0) x = anat A (fold A nat (ab nat) x)).
+Abort.
+
+End mult.
+
+(** Current semantics for rewriting with typeclass constraints in the lemma 
+   does not fix the instance at the first unification, use [at], or simply rewrite for 
+   this semantics. *)
+
+Require Import Arith.
+
+Class Foo (A : Type) := {foo_neg : A -> A ; foo_prf : forall x : A, x = foo_neg x}.
+Instance: Foo nat. admit. Defined.
+Instance: Foo bool. admit. Defined.
+
+Goal forall (x : nat) (y : bool), beq_nat (foo_neg x) 0 = foo_neg y.
+Proof. intros. setoid_rewrite <- foo_prf. change (beq_nat x 0 = y). Abort.
+
+Goal forall (x : nat) (y : bool), beq_nat (foo_neg x) 0 = foo_neg y.
+Proof. intros. setoid_rewrite <- @foo_prf at 1. change (beq_nat x 0 = foo_neg y). Abort.
+
diff --git a/test-suite/success/simpl_tuning.v b/test-suite/success/simpl_tuning.v
new file mode 100644
index 00000000..d4191b93
--- /dev/null
+++ b/test-suite/success/simpl_tuning.v
@@ -0,0 +1,149 @@
+(* as it is dynamically inferred by simpl *)
+Arguments minus !n / m.
+
+Lemma foo x y : S (S x) - S y = 0.
+simpl.
+match goal with |- (match y with O => S x | S _ => _ end = 0) => idtac end.
+Abort. 
+
+(* we avoid exposing a match *)
+Arguments minus n m : simpl nomatch. 
+
+Lemma foo x : minus 0 x = 0.
+simpl.
+match goal with |- (0 = 0) => idtac end.
+Abort.
+
+Lemma foo x y : S (S x) - S y = 0.
+simpl.
+match goal with |- (S x - y = 0) => idtac end.
+Abort.
+
+Lemma foo x y : S (S x) - (S (match y with O => O | S z => S z end)) = 0.
+simpl.
+match goal with |-(S x - (match y with O => _ | S _ => _ end) = 0) => idtac end.
+Abort.
+
+(* we unfold as soon as we have 1 args, but we avoid exposing a match *)
+Arguments minus n / m : simpl nomatch. 
+
+Lemma foo : minus 0 = fun x => 0.
+simpl.
+match goal with |- minus 0 = _ => idtac end.
+Abort.
+(* This does not work as one may expect. The point is that simpl is implemented
+   as "strong (whd_simpl_state)" and after unfolding minus you have
+   (fun m => match 0 => 0 | S n => ...) that is already in whd and exposes
+   a match, that of course "strong" would reduce away but at that stage
+   we don't know, and reducing by hand under the lambda is against whd *) 
+
+(* extra tuning for the usual heuristic *)
+Arguments minus !n / m : simpl nomatch. 
+
+Lemma foo x y : S (S x) - S y = 0.
+simpl.
+match goal with |- (S x - y = 0) => idtac end.
+Abort.
+
+Lemma foo x y : S (S x) - (S (match y with O => O | S z => S z end)) = 0.
+simpl.
+match goal with |-(S x - (match y with O => _ | S _ => _ end) = 0) => idtac end.
+Abort.
+
+(* full control *)
+Arguments minus !n !m /.
+
+Lemma foo x y : S (S x) - S y = 0.
+simpl.
+match goal with |- (S x - y = 0) => idtac end.
+Abort.
+
+Lemma foo x y : S (S x) - (S (match y with O => O | S z => S z end)) = 0.
+simpl.
+match goal with |-(S x - (match y with O => _ | S _ => _ end) = 0) => idtac end.
+Abort.
+
+(* omitting /, that being immediately after the last ! is irrelevant *)
+Arguments minus !n !m.
+
+Lemma foo x y : S (S x) - S y = 0.
+simpl.
+match goal with |- (S x - y = 0) => idtac end.
+Abort.
+
+Lemma foo x y : S (S x) - (S (match y with O => O | S z => S z end)) = 0.
+simpl.
+match goal with |-(S x - (match y with O => _ | S _ => _ end) = 0) => idtac end.
+Abort.
+
+Definition pf (D1 C1 : Type) (f : D1 -> C1) (D2 C2 : Type) (g : D2 -> C2) := 
+  fun x => (f (fst x), g (snd x)).
+
+Delimit Scope foo_scope with F.
+Notation "@@" := nat (only parsing) : foo_scope.
+Notation "@@" := (fun x => x) (only parsing).
+
+Arguments pf {D1%F C1%type} f [D2 C2] g x : simpl never.
+
+Lemma foo x : @pf @@ nat @@ nat nat @@ x = pf @@ @@ x.
+Abort.
+
+Definition fcomp A B C f (g : A -> B) (x : A) : C := f (g x).
+
+(* fcomp is unfolded if applied to 6 args *)
+Arguments fcomp {A B C}%type f g x /.
+
+Notation "f \o g" := (fcomp f g) (at level 50).
+
+Lemma foo (f g h : nat -> nat) x : pf (f \o g) h x = pf f h (g (fst x), snd x).
+simpl.
+match goal with |- (pf (f \o g) h x = _) => idtac end.
+case x; intros x1 x2. 
+simpl.
+match goal with |- (pf (f \o g) h _ = pf f h _) => idtac end.
+unfold pf; simpl.
+match goal with |- (f (g x1), h x2) = (f (g x1), h x2) => idtac end.
+Abort. 
+
+Definition volatile := fun x : nat => x.
+Arguments volatile /.
+
+Lemma foo : volatile = volatile.
+simpl.
+match goal with |- (fun _ => _) = _ => idtac end.
+Abort.
+
+Set Implicit Arguments.
+
+Section S1.
+
+Variable T1 : Type.
+
+Section S2.
+
+Variable T2 : Type.
+
+Fixpoint f (x : T1) (y : T2) n (v : unit) m {struct n} : nat :=
+  match n, m with
+  | 0,_ => 0
+  | S _, 0 => n
+  | S n', S m' => f x y n' v m' end.
+
+Global Arguments f x y !n !v !m.
+
+Lemma foo x y n m : f x y (S n) tt m = f x y (S n) tt (S m).
+simpl.
+match goal with |- (f _ _ _ _ _ = f _ _ _ _ _) => idtac end.
+Abort.
+
+End S2.
+
+Lemma foo T x y n m : @f T x y (S n) tt m = @f T x y (S n) tt (S m).
+simpl.
+match goal with |- (f _ _ _ _ _ = f _ _ _ _ _) => idtac end.
+Abort.
+
+End S1.
+
+Arguments f : clear implicits and scopes.
+
diff --git a/test-suite/success/telescope_canonical.v b/test-suite/success/telescope_canonical.v
new file mode 100644
index 00000000..8a607c93
--- /dev/null
+++ b/test-suite/success/telescope_canonical.v
@@ -0,0 +1,12 @@
+Structure Inner := mkI { is :> Type }.
+Structure Outer := mkO { os :> Inner }.
+
+Canonical Structure natInner := mkI nat.
+Canonical Structure natOuter := mkO natInner.
+
+Definition hidden_nat := nat.
+
+Axiom P : forall S : Outer, is (os S) -> Prop.
+
+Lemma foo (n : hidden_nat) : P _ n.
+Admitted.
diff --git a/test-suite/success/unfold.v b/test-suite/success/unfold.v
index 66c4e080..5649e2f7 100644
--- a/test-suite/success/unfold.v
+++ b/test-suite/success/unfold.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/test-suite/success/unification.v b/test-suite/success/unification.v
index ddf122e8..997dceb4 100644
--- a/test-suite/success/unification.v
+++ b/test-suite/success/unification.v
@@ -21,6 +21,12 @@ Proof.
 intros; apply H.
 Qed.
 
+  (* Feature introduced June 2011 *)
+
+Lemma l7 : forall x (P:nat->Prop), (forall f, P (f x)) -> P (x+x).
+Proof.
+intros x P H; apply H.
+Qed.
 
 (* Example submitted for Zenon *)
 
@@ -90,12 +96,14 @@ intros.
 apply H.
 Qed.
 
+(* Feature deactivated in commit 14189 (see commit log)
 (* Test instanciation of evars by unification *)
 
 Goal (forall x, 0 + x = 0 -> True) -> True.
 intros; eapply H.
 rewrite <- plus_n_Sm. (* should refine ?x with S ?x' *)
 Abort.
+*)
 
 (* Check handling of identity equation between evars *)
 (* The example failed to pass until revision 10623 *)
@@ -135,4 +143,44 @@ Goal (forall (A B : Set) (f : A -> B), (fun x => f x) = f) ->
  forall (A B C : Set) (g : (A -> B) -> C) (f : A -> B), g (fun x => f x) = g f.
 Proof.
   intros.
-  rewrite H.
+  rewrite H with (f:=f0).
+Abort.
+
+(* Three tests provided by Dan Grayson as part of a custom patch he
+   made for a more powerful "destruct" for handling Voevodsky's
+   Univalent Foundations. The test checks if second-order matching in
+   tactic unification is able to guess by itself on which dependent
+   terms to abstract so that the elimination predicate is well-typed *)
+
+Definition test1 (X : Type) (x : X) (fxe : forall x1 : X, identity x1 x1) :
+  identity (fxe x) (fxe x).
+Proof. destruct (fxe x). apply identity_refl. Defined.
+
+(* a harder example *)
+
+Definition UU := Type .
+Inductive paths {T:Type}(t:T): T -> UU := idpath: paths t t.
+Inductive foo (X0:UU) (x0:X0) : forall (X:UU)(x:X), UU := newfoo : foo x0 x0.
+Definition idonfoo {X0:UU} {x0:X0} {X1:UU} {x1:X1} : foo x0 x1 -> foo x0 x1.
+Proof. intros t. exact t. Defined.
+
+Lemma test2 (T:UU) (t:T) (k : foo t t) : paths k (idonfoo k).
+Proof.
+  destruct k.
+  apply idpath.
+Defined.
+
+(* an example with two constructors *)
+
+Inductive foo' (X0:UU) (x0:X0) : forall (X:UU)(x:X), UU :=
+| newfoo1 : foo' x0 x0
+| newfoo2 : foo' x0 x0 .
+Definition idonfoo' {X0:UU} {x0:X0} {X1:UU} {x1:X1} :
+  foo' x0 x1 -> foo' x0 x1.
+Proof. intros t. exact t. Defined.
+Lemma test3 (T:UU) (t:T) (k : foo' t t) : paths k (idonfoo' k).
+Proof.
+  destruct k.
+  apply idpath.
+  apply idpath.
+Defined.
diff --git a/test-suite/success/universes-coercion.v b/test-suite/success/universes-coercion.v
new file mode 100644
index 00000000..d7504340
--- /dev/null
+++ b/test-suite/success/universes-coercion.v
@@ -0,0 +1,22 @@
+(* This example used to emphasize the absence of LEGO-style universe
+   polymorphism; Matthieu's improvements of typing on 2011/3/11 now
+   makes (apparently) that Amokrane's automatic eta-expansion in the
+   coercion mechanism works; this makes its illustration as a "weakness"
+   of universe polymorphism obsolete (example submitted by Randy Pollack).
+
+   Note that this example is not an evidence that the current
+   non-kernel eta-expansion behavior is the most expected one.  
+*)
+
+Parameter K : forall T : Type, T -> T.
+Check (K (forall T : Type, T -> T) K).
+
+(*
+   note that the inferred term is
+     "(K (forall T (* u1 *) : Type, T -> T) (fun T:Type (* u1 *) => K T))"
+   which is not eta-equivalent to 
+     "(K (forall T : Type, T -> T) K"
+   because the eta-expansion of the latter
+     "(K (forall T : Type, T -> T) (fun T:Type (* u2 *) => K T)"
+  assuming K of type "forall T (* u2 *) : Type, T -> T"
+*)
diff --git a/test-suite/typeclasses/NewSetoid.v b/test-suite/typeclasses/NewSetoid.v
index cc40ae07..3fdcce6f 100644
--- a/test-suite/typeclasses/NewSetoid.v
+++ b/test-suite/typeclasses/NewSetoid.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -11,8 +11,6 @@
  * Institution: LRI, CNRS UMR 8623 - Universit�copyright Paris Sud
  *              91405 Orsay, France *)
 
-(* $Id: FSetAVL_prog.v 616 2007-08-08 12:28:10Z msozeau $ *)
-
 Require Import Coq.Program.Program.
 
 Set Implicit Arguments.
author	Stephane Glondu <steph@glondu.net>	2012-01-12 16:02:20 +0100
committer	Stephane Glondu <steph@glondu.net>	2012-01-12 16:02:20 +0100
commit	97fefe1fcca363a1317e066e7f4b99b9c1e9987b (patch)
tree	97ec6b7d831cc5fb66328b0c63a11db1cbb2f158 /test-suite
parent	300293c119981054c95182a90c829058530a6b6f (diff)