Imported Upstream version 8.4~betaupstream/8.4_beta

32 files changed, 688 insertions, 63 deletions

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.