summaryrefslogtreecommitdiff
path: root/test-suite/output
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2012-01-12 16:02:20 +0100
committerGravatar Stephane Glondu <steph@glondu.net>2012-01-12 16:02:20 +0100
commit97fefe1fcca363a1317e066e7f4b99b9c1e9987b (patch)
tree97ec6b7d831cc5fb66328b0c63a11db1cbb2f158 /test-suite/output
parent300293c119981054c95182a90c829058530a6b6f (diff)
Imported Upstream version 8.4~betaupstream/8.4_beta
Diffstat (limited to 'test-suite/output')
-rw-r--r--test-suite/output/Arguments.out93
-rw-r--r--test-suite/output/Arguments.v40
-rw-r--r--test-suite/output/ArgumentsScope.out5
-rw-r--r--test-suite/output/Arguments_renaming.out108
-rw-r--r--test-suite/output/Arguments_renaming.v54
-rw-r--r--test-suite/output/Errors.out2
-rw-r--r--test-suite/output/Errors.v9
-rw-r--r--test-suite/output/Existentials.out4
-rw-r--r--test-suite/output/Fixpoint.out15
-rw-r--r--test-suite/output/Fixpoint.v8
-rw-r--r--test-suite/output/Implicit.out2
-rw-r--r--test-suite/output/Implicit.v17
-rw-r--r--test-suite/output/InitSyntax.out2
-rw-r--r--test-suite/output/Notations.out16
-rw-r--r--test-suite/output/Notations.v8
-rw-r--r--test-suite/output/Notations2.out25
-rw-r--r--test-suite/output/Notations2.v26
-rw-r--r--test-suite/output/NumbersSyntax.out14
-rw-r--r--test-suite/output/PrintInfos.out129
-rw-r--r--test-suite/output/PrintInfos.v41
-rw-r--r--test-suite/output/Record.out16
-rw-r--r--test-suite/output/Record.v21
-rw-r--r--test-suite/output/Search.out6
-rw-r--r--test-suite/output/SearchPattern.out8
-rw-r--r--test-suite/output/Tactics.out10
-rw-r--r--test-suite/output/Tactics.v13
-rw-r--r--test-suite/output/ZSyntax.out8
-rw-r--r--test-suite/output/ZSyntax.v8
-rw-r--r--test-suite/output/inference.out6
-rw-r--r--test-suite/output/inference.v14
-rw-r--r--test-suite/output/rewrite-2172.out2
-rw-r--r--test-suite/output/rewrite-2172.v21
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.