diff options
Diffstat (limited to 'test-suite/output')
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. |