diff options
Diffstat (limited to 'test-suite/output')
42 files changed, 126 insertions, 339 deletions
diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out index a35885651..63137edba 100644 --- a/test-suite/output/Cases.out +++ b/test-suite/output/Cases.out @@ -1,6 +1,9 @@ t_rect = -[P:(t ->Type); f:([x:=t](x0:x)(P x0) ->(P (k x0)))] - Fix F - {F [t:t] : (P t) := <[t0:t](P t0)>Cases t of (k x x0) => (f x0 (F x0)) end} - : (P:(t ->Type))([x:=t](x0:x)(P x0) ->(P (k x0))) ->(t:t)(P t) +fun (P : t -> Type) (f : let x := t in forall x0 : x, P x0 -> P (k x0)) => +fix F (t : t) : P t := + match t as t0 return (P t0) with + | k x x0 => f x0 (F x0) + end + : forall P : t -> Type, + (let x := t in forall x0 : x, P x0 -> P (k x0)) -> forall t : t, P t diff --git a/test-suite/output/Cases.out8 b/test-suite/output/Cases.out8 deleted file mode 100644 index b63ffd926..000000000 --- a/test-suite/output/Cases.out8 +++ /dev/null @@ -1,13 +0,0 @@ -t_rect = -fun (P : t -> Type) (f : let x := t in forall x0 : x, P x0 -> P (k x0)) => -fix F (t : t) : P t := - match t as t0 return (P t0) with - | k x x0 => f x0 (F x0) - end - : forall P : t -> Type, - (let x := t in forall x0 : x, P x0 -> P (k x0)) -> forall t : t, P t - - = (1, 3) - : (nat * nat)%type - = (1, 2) - : (nat * nat)%type diff --git a/test-suite/output/Cases.v b/test-suite/output/Cases.v index 7483e8c40..452d36036 100644 --- a/test-suite/output/Cases.v +++ b/test-suite/output/Cases.v @@ -1,5 +1,6 @@ (* Cases with let-in in constructors types *) -Inductive t : Set := k : [x:=t]x -> x. +Inductive t : Set := + k : let x := t in x -> x. Print t_rect. diff --git a/test-suite/output/Cases.v8 b/test-suite/output/Cases.v8 deleted file mode 100644 index f62206358..000000000 --- a/test-suite/output/Cases.v8 +++ /dev/null @@ -1,6 +0,0 @@ -(* Cases with let-in in constructors types *) - -Inductive t : Set := - k : let x := t in x -> x. - -Print t_rect.
\ No newline at end of file diff --git a/test-suite/output/Coercions.out b/test-suite/output/Coercions.out index 9f0979b74..4b8aa355a 100644 --- a/test-suite/output/Coercions.out +++ b/test-suite/output/Coercions.out @@ -1,6 +1,6 @@ -(P x) +P x : Prop -(R x x) +R x x : Prop -[x:foo; n:nat](x n) - : foo ->nat ->nat +fun (x : foo) (n : nat) => x n + : foo -> nat -> nat diff --git a/test-suite/output/Coercions.out8 b/test-suite/output/Coercions.out8 deleted file mode 100644 index 4b8aa355a..000000000 --- a/test-suite/output/Coercions.out8 +++ /dev/null @@ -1,6 +0,0 @@ -P x - : Prop -R x x - : Prop -fun (x : foo) (n : nat) => x n - : foo -> nat -> nat diff --git a/test-suite/output/Coercions.v b/test-suite/output/Coercions.v index 2ad8b924e..c88b143f8 100644 --- a/test-suite/output/Coercions.v +++ b/test-suite/output/Coercions.v @@ -1,15 +1,15 @@ (* Submitted by Randy Pollack *) -Record pred [S:Set]: Type := { sp_pred :> S -> Prop }. -Record rel [S:Set]: Type := { sr_rel :> S -> S -> Prop }. +Record pred (S : Set) : Type := {sp_pred :> S -> Prop}. +Record rel (S : Set) : Type := {sr_rel :> S -> S -> Prop}. Section testSection. -Variables S: Set; P: (pred S); R: (rel S); x:S. +Variables (S : Set) (P : pred S) (R : rel S) (x : S). Check (P x). Check (R x x). End testSection. (* Check the removal of coercions with target Funclass *) -Record foo : Type := { D :> nat -> nat }. -Check [x:foo;n:nat](x n). +Record foo : Type := {D :> nat -> nat}. +Check (fun (x : foo) (n : nat) => x n). diff --git a/test-suite/output/Coercions.v8 b/test-suite/output/Coercions.v8 deleted file mode 100644 index f3a09f3c2..000000000 --- a/test-suite/output/Coercions.v8 +++ /dev/null @@ -1,15 +0,0 @@ -(* Submitted by Randy Pollack *) - -Record pred (S : Set) : Type := {sp_pred :> S -> Prop}. -Record rel (S : Set) : Type := {sr_rel :> S -> S -> Prop}. - -Section testSection. -Variables (S : Set) (P : pred S) (R : rel S) (x : S). -Check (P x). -Check (R x x). -End testSection. - -(* Check the removal of coercions with target Funclass *) - -Record foo : Type := {D :> nat -> nat}. -Check (fun (x : foo) (n : nat) => x n).
\ No newline at end of file diff --git a/test-suite/output/Fixpoint.out b/test-suite/output/Fixpoint.out index 9873ad533..5af28a5af 100644 --- a/test-suite/output/Fixpoint.out +++ b/test-suite/output/Fixpoint.out @@ -1,7 +1,11 @@ -Fix F - {F [A,B:Set; f:(A ->B); l:(list A)] : (list B) := - Cases l of - nil => (nil B) - | (cons a l0) => (cons (f a) (F A B f l0)) - end} - : (A,B:Set)(A ->B) ->(list A) ->(list B) +fix F (A B : Set) (f : A -> B) (l : list A) {struct l} : +list B := match l with + | nil => nil (A:=B) + | a :: l0 => f a :: F A B f l0 + end + : forall A B : Set, (A -> B) -> list A -> list B +let fix f (m : nat) : nat := match m with + | O => 0 + | S m' => f m' + end in f 0 + : nat diff --git a/test-suite/output/Fixpoint.out8 b/test-suite/output/Fixpoint.out8 deleted file mode 100644 index 5af28a5af..000000000 --- a/test-suite/output/Fixpoint.out8 +++ /dev/null @@ -1,11 +0,0 @@ -fix F (A B : Set) (f : A -> B) (l : list A) {struct l} : -list B := match l with - | nil => nil (A:=B) - | a :: l0 => f a :: F A B f l0 - end - : forall A B : Set, (A -> B) -> list A -> list B -let fix f (m : nat) : nat := match m with - | O => 0 - | S m' => f m' - end in f 0 - : nat diff --git a/test-suite/output/Fixpoint.v b/test-suite/output/Fixpoint.v index 270fff4ef..fc27e8d28 100644 --- a/test-suite/output/Fixpoint.v +++ b/test-suite/output/Fixpoint.v @@ -1,7 +1,18 @@ -Require PolyList. +Require Import List. + +Check + (fix F (A B : Set) (f : A -> B) (l : list A) {struct l} : + list B := match l with + | nil => nil + | a :: l => f a :: F _ _ f l + end). + +(* V8 printing of this term used to failed in V8.0 and V8.0pl1 (cf bug #860) *) +Check + let fix f (m : nat) : nat := + match m with + | O => 0 + | S m' => f m' + end + in f 0. -Check Fix F { F/4 : (A,B:Set)(A->B)->(list A)->(list B) := - [_,_,f,l]Cases l of - nil => (nil ?) - | (cons a l) => (cons (f a) (F ? ? f l)) - end}. diff --git a/test-suite/output/Fixpoint.v8 b/test-suite/output/Fixpoint.v8 deleted file mode 100644 index ab1467a56..000000000 --- a/test-suite/output/Fixpoint.v8 +++ /dev/null @@ -1,17 +0,0 @@ -Require Import List. - -Check - (fix F (A B : Set) (f : A -> B) (l : list A) {struct l} : - list B := match l with - | nil => nil - | a :: l => f a :: F _ _ f l - end). - -(* V8 printing of this term used to failed in V8.0 and V8.0pl1 (cf bug #860) *) -Check - let fix f (m : nat) : nat := - match m with - | O => 0 - | S m' => f m' - end - in f 0. diff --git a/test-suite/output/Implicit.out b/test-suite/output/Implicit.out index f5c812c8a..38c5b827f 100644 --- a/test-suite/output/Implicit.out +++ b/test-suite/output/Implicit.out @@ -1,10 +1,10 @@ -(compose 3!nat S) - : (nat ->nat) ->nat ->nat -(ex_intro 2![_:nat]True 3!(0) I) - : (ex [_:nat]True) -d2 = [x:nat](d1 1!x) - : (x,x0:nat)x0=x ->x0=x +compose (C:=nat) S + : (nat -> nat) -> nat -> nat +ex_intro (P:=fun _ : nat => True) (x:=0) I + : ex (fun _ : nat => True) +d2 = fun x : nat => d1 (y:=x) + : forall x x0 : nat, x0 = x -> x0 = x -Positions [1; 2] are implicit +Arguments x, x0 are implicit Argument scopes are [nat_scope nat_scope _] diff --git a/test-suite/output/Implicit.out8 b/test-suite/output/Implicit.out8 deleted file mode 100644 index 38c5b827f..000000000 --- a/test-suite/output/Implicit.out8 +++ /dev/null @@ -1,10 +0,0 @@ -compose (C:=nat) S - : (nat -> nat) -> nat -> nat -ex_intro (P:=fun _ : nat => True) (x:=0) I - : ex (fun _ : nat => True) -d2 = fun x : nat => d1 (y:=x) - : forall x x0 : nat, x0 = x -> x0 = x - - -Arguments x, x0 are implicit -Argument scopes are [nat_scope nat_scope _] diff --git a/test-suite/output/Implicit.v b/test-suite/output/Implicit.v index 2dea0d185..0ff7e87f3 100644 --- a/test-suite/output/Implicit.v +++ b/test-suite/output/Implicit.v @@ -1,18 +1,19 @@ Set Implicit Arguments. +Unset Strict Implicit. (* Suggested by Pierre Casteran (bug #169) *) (* Argument 3 is needed to typecheck and should be printed *) -Definition compose := [A,B,C:Set; f : A-> B ; g : B->C ; x : A] (g (f x)). -Check (compose 3!nat S). +Definition compose (A B C : Set) (f : A -> B) (g : B -> C) (x : A) := g (f x). +Check (compose (C:=nat) S). (* Better to explicitly display the arguments inferable from a position that could disappear after reduction *) -Inductive ex [A:Set;P:A->Prop] : Prop - := ex_intro : (x:A)(P x)->(ex P). -Check (ex_intro 2![_]True 3!O I). +Inductive ex (A : Set) (P : A -> Prop) : Prop := + ex_intro : forall x : A, P x -> ex P. +Check (ex_intro (P:=fun _ => True) (x:=0) I). (* Test for V8 printing of implicit by names *) -Definition d1 [y;x;h:x=y:>nat] := h. -Definition d2 [x] := (!d1 x). +Definition d1 y x (h : x = y :>nat) := h. +Definition d2 x := d1 (y:=x). Print d2. diff --git a/test-suite/output/Implicit.v8 b/test-suite/output/Implicit.v8 deleted file mode 100644 index e18ae5513..000000000 --- a/test-suite/output/Implicit.v8 +++ /dev/null @@ -1,19 +0,0 @@ -Set Implicit Arguments. -Unset Strict Implicit. - -(* Suggested by Pierre Casteran (bug #169) *) -(* Argument 3 is needed to typecheck and should be printed *) -Definition compose (A B C : Set) (f : A -> B) (g : B -> C) (x : A) := g (f x). -Check (compose (C:=nat) S). - -(* Better to explicitly display the arguments inferable from a - position that could disappear after reduction *) -Inductive ex (A : Set) (P : A -> Prop) : Prop := - ex_intro : forall x : A, P x -> ex P. -Check (ex_intro (P:=fun _ => True) (x:=0) I). - -(* Test for V8 printing of implicit by names *) -Definition d1 y x (h : x = y :>nat) := h. -Definition d2 x := d1 (y:=x). - -Print d2.
\ No newline at end of file diff --git a/test-suite/output/InitSyntax.out b/test-suite/output/InitSyntax.out index 79ddf8c44..4ed72c506 100644 --- a/test-suite/output/InitSyntax.out +++ b/test-suite/output/InitSyntax.out @@ -1,8 +1,10 @@ -Inductive sig2 [A : Set; P : A ->Prop; Q : A ->Prop] : Set := - exist2 : (x:A)(P x) ->(Q x) ->(sig2 A P Q) +Inductive sig2 (A : Set) (P : A -> Prop) (Q : A -> Prop) : Set := + exist2 : forall x : A, P x -> Q x -> sig2 P Q +For sig2: Argument A is implicit +For exist2: Argument A is implicit For sig2: Argument scopes are [type_scope type_scope type_scope] For exist2: Argument scopes are [type_scope _ _ _ _ _] -(EX x:nat|x=x) +exists x : nat, x = x : Prop -[b:bool](if b then b else b) - : bool ->bool +fun b : bool => if b then b else b + : bool -> bool diff --git a/test-suite/output/InitSyntax.out8 b/test-suite/output/InitSyntax.out8 deleted file mode 100644 index 4ed72c506..000000000 --- a/test-suite/output/InitSyntax.out8 +++ /dev/null @@ -1,10 +0,0 @@ -Inductive sig2 (A : Set) (P : A -> Prop) (Q : A -> Prop) : Set := - exist2 : forall x : A, P x -> Q x -> sig2 P Q -For sig2: Argument A is implicit -For exist2: Argument A is implicit -For sig2: Argument scopes are [type_scope type_scope type_scope] -For exist2: Argument scopes are [type_scope _ _ _ _ _] -exists x : nat, x = x - : Prop -fun b : bool => if b then b else b - : bool -> bool diff --git a/test-suite/output/InitSyntax.v b/test-suite/output/InitSyntax.v index 90fad3718..eb39782ec 100644 --- a/test-suite/output/InitSyntax.v +++ b/test-suite/output/InitSyntax.v @@ -1,4 +1,4 @@ (* Soumis par Pierre *) -Print sig2. -Check (EX x:nat|x=x). -Check [b:bool]if b then b else b. +Print sig2. +Check (exists x : nat, x = x). +Check (fun b : bool => if b then b else b). diff --git a/test-suite/output/InitSyntax.v8 b/test-suite/output/InitSyntax.v8 deleted file mode 100644 index 66a01e145..000000000 --- a/test-suite/output/InitSyntax.v8 +++ /dev/null @@ -1,4 +0,0 @@ -(* Soumis par Pierre *) -Print sig2. -Check (exists x : nat, x = x). -Check (fun b : bool => if b then b else b).
\ No newline at end of file diff --git a/test-suite/output/Intuition.out b/test-suite/output/Intuition.out index cadb35c63..5831c9f43 100644 --- a/test-suite/output/Intuition.out +++ b/test-suite/output/Intuition.out @@ -2,6 +2,6 @@ m : Z n : Z - H : `m >= n` + H : (m >= n)%Z ============================ - `m >= m` + (m >= m)%Z diff --git a/test-suite/output/Intuition.out8 b/test-suite/output/Intuition.out8 deleted file mode 100644 index 5831c9f43..000000000 --- a/test-suite/output/Intuition.out8 +++ /dev/null @@ -1,7 +0,0 @@ -1 subgoal - - m : Z - n : Z - H : (m >= n)%Z - ============================ - (m >= m)%Z diff --git a/test-suite/output/Intuition.v b/test-suite/output/Intuition.v index c0508c90b..5f1914d21 100644 --- a/test-suite/output/Intuition.v +++ b/test-suite/output/Intuition.v @@ -1,5 +1,5 @@ -Require ZArith_base. -Goal (m,n:Z) `m >= n` -> `m >= m` /\ `m >= n`. -Intros; Intuition. +Require Import ZArith_base. +Goal forall m n : Z, (m >= n)%Z -> (m >= m)%Z /\ (m >= n)%Z. +intros; intuition. Show. Abort. diff --git a/test-suite/output/Intuition.v8 b/test-suite/output/Intuition.v8 deleted file mode 100644 index d9d35cabc..000000000 --- a/test-suite/output/Intuition.v8 +++ /dev/null @@ -1,5 +0,0 @@ -Require Import ZArith_base. -Goal forall m n : Z, (m >= n)%Z -> (m >= m)%Z /\ (m >= n)%Z. -intros; intuition. -Show. -Abort.
\ No newline at end of file diff --git a/test-suite/output/Nametab.out8 b/test-suite/output/Nametab.out8 deleted file mode 100644 index f5e76e449..000000000 --- a/test-suite/output/Nametab.out8 +++ /dev/null @@ -1,28 +0,0 @@ -Constant Top.Q.N.K.id (shorter name to refer to it is Q.N.K.id) -Constant Top.Q.N.K.id (shorter name to refer to it is Q.N.K.id) -Constant Top.Q.N.K.id (shorter name to refer to it is Q.N.K.id) -Constant Top.Q.N.K.id -Constant Top.Q.N.K.id (shorter name to refer to it is Q.N.K.id) -No module is referred to by basename K -No module is referred to by name N.K -Module Top.Q.N.K -Module Top.Q.N.K -No module is referred to by basename N -Module Top.Q.N -Module Top.Q.N -Module Top.Q -Module Top.Q -Constant Top.Q.N.K.id (shorter name to refer to it is K.id) -Constant Top.Q.N.K.id -Constant Top.Q.N.K.id (shorter name to refer to it is K.id) -Constant Top.Q.N.K.id (shorter name to refer to it is K.id) -Constant Top.Q.N.K.id (shorter name to refer to it is K.id) -Module Top.Q.N.K -No module is referred to by name N.K -Module Top.Q.N.K -Module Top.Q.N.K -No module is referred to by basename N -Module Top.Q.N -Module Top.Q.N -Module Top.Q -Module Top.Q diff --git a/test-suite/output/Nametab.v8 b/test-suite/output/Nametab.v index e36881e86..8aed87a52 100644 --- a/test-suite/output/Nametab.v8 +++ b/test-suite/output/Nametab.v @@ -4,4 +4,4 @@ Module Q. Definition id := Set. End K. End N. -End Q.
\ No newline at end of file +End Q. diff --git a/test-suite/output/Notations.out8 b/test-suite/output/Notations.out8 deleted file mode 100644 index 0e57e269d..000000000 --- a/test-suite/output/Notations.out8 +++ /dev/null @@ -1,16 +0,0 @@ -true ? 0; 1 - : nat -if true as x return (x ? nat; bool) then 0 else true - : true ? nat; bool -Defining 'proj1' as keyword -fun e : nat * nat => proj1 e - : nat * nat -> nat -Defining 'decomp' as keyword -decomp (true, true) as t, u in (t, u) - : (bool * bool)%type -!(0 = 0) - : Prop -forall n : nat, n = 0 - : Prop -!(0 = 0) - : Prop diff --git a/test-suite/output/Notations.v8 b/test-suite/output/Notations.v index e5b469dba..deb3bb078 100644 --- a/test-suite/output/Notations.v8 +++ b/test-suite/output/Notations.v @@ -20,3 +20,4 @@ Notation "! A" := (forall _:nat, A) (at level 60). Check ! (0=0). Check forall n, n=0. Check forall n:nat, 0=0. + diff --git a/test-suite/output/RealSyntax.out b/test-suite/output/RealSyntax.out index fa30656bf..e6f7556d9 100644 --- a/test-suite/output/RealSyntax.out +++ b/test-suite/output/RealSyntax.out @@ -1,4 +1,4 @@ -``32`` +32%R : R -``-31`` +(-31)%R : R diff --git a/test-suite/output/RealSyntax.out8 b/test-suite/output/RealSyntax.out8 deleted file mode 100644 index e6f7556d9..000000000 --- a/test-suite/output/RealSyntax.out8 +++ /dev/null @@ -1,4 +0,0 @@ -32%R - : R -(-31)%R - : R diff --git a/test-suite/output/RealSyntax.v b/test-suite/output/RealSyntax.v index d976dcc1a..15ae66010 100644 --- a/test-suite/output/RealSyntax.v +++ b/test-suite/output/RealSyntax.v @@ -1,3 +1,3 @@ -Require Reals. -Check ``32``. -Check ``-31``. +Require Import Reals. +Check 32%R. +Check (-31)%R. diff --git a/test-suite/output/RealSyntax.v8 b/test-suite/output/RealSyntax.v8 deleted file mode 100644 index 2e4feeef0..000000000 --- a/test-suite/output/RealSyntax.v8 +++ /dev/null @@ -1,3 +0,0 @@ -Require Import Reals. -Check 32%R. -Check (-31)%R.
\ No newline at end of file diff --git a/test-suite/output/Sum.out b/test-suite/output/Sum.out index e8b215bc7..bda6a68b0 100644 --- a/test-suite/output/Sum.out +++ b/test-suite/output/Sum.out @@ -1,6 +1,6 @@ -'type:nat+nat '+{True} +nat + nat + {True} : Set -{True}+{True}+{True} +{True} + {True} + {True} : Set -nat+{True}+{True} +nat + {True} + {True} : Set diff --git a/test-suite/output/Sum.out8 b/test-suite/output/Sum.out8 deleted file mode 100644 index bda6a68b0..000000000 --- a/test-suite/output/Sum.out8 +++ /dev/null @@ -1,6 +0,0 @@ -nat + nat + {True} - : Set -{True} + {True} + {True} - : Set -nat + {True} + {True} - : Set diff --git a/test-suite/output/Sum.v b/test-suite/output/Sum.v index aceadd121..f12285a60 100644 --- a/test-suite/output/Sum.v +++ b/test-suite/output/Sum.v @@ -1,3 +1,3 @@ -Check nat+nat+{True}. -Check {True}+{True}+{True}. -Check nat+{True}+{True}. +Check (nat + nat + {True}). +Check ({True} + {True} + {True}). +Check (nat + {True} + {True}). diff --git a/test-suite/output/Sum.v8 b/test-suite/output/Sum.v8 deleted file mode 100644 index c13f975b7..000000000 --- a/test-suite/output/Sum.v8 +++ /dev/null @@ -1,3 +0,0 @@ -Check (nat + nat + {True}). -Check ({True} + {True} + {True}). -Check (nat + {True} + {True}).
\ No newline at end of file diff --git a/test-suite/output/TranspModtype.out8 b/test-suite/output/TranspModtype.out8 deleted file mode 100644 index 41e8648bc..000000000 --- a/test-suite/output/TranspModtype.out8 +++ /dev/null @@ -1,10 +0,0 @@ -TrM.A = M.A - : Set - -OpM.A = M.A - : Set - -TrM.B = M.B - : Set - -*** [ OpM.B : Set ] diff --git a/test-suite/output/TranspModtype.v8 b/test-suite/output/TranspModtype.v index 27a1dff06..68eff33a6 100644 --- a/test-suite/output/TranspModtype.v8 +++ b/test-suite/output/TranspModtype.v @@ -19,4 +19,4 @@ Module OpM := OpaqueId M. Print TrM.A. Print OpM.A. Print TrM.B. -Print OpM.B.
\ No newline at end of file +Print OpM.B. diff --git a/test-suite/output/ZSyntax.out b/test-suite/output/ZSyntax.out index e856686ac..cbfb9f207 100644 --- a/test-suite/output/ZSyntax.out +++ b/test-suite/output/ZSyntax.out @@ -1,26 +1,26 @@ -`32` +32%Z : Z -[f:(nat ->Z)]`(f O)+0` - : (nat ->Z) ->Z -[x:positive](POS (xO x)) - : positive ->Z -[x:positive]`(POS x)+1` - : positive ->Z -[x:positive](POS x) - : positive ->Z -[x:positive](NEG (xO x)) - : positive ->Z -[x:positive]`(POS (xO x))+0` - : positive ->Z -[x:positive]`(Zopp (POS (xO x)))` - : positive ->Z -[x:positive]`(Zopp (POS (xO x)))+0` - : positive ->Z -`(inject_nat (0))+1` +fun f : nat -> Z => (f 0%nat + 0)%Z + : (nat -> Z) -> Z +fun x : positive => Zpos (xO x) + : positive -> Z +fun x : positive => (Zpos x + 1)%Z + : positive -> Z +fun x : positive => Zpos x + : positive -> Z +fun x : positive => Zneg (xO x) + : positive -> Z +fun x : positive => (Zpos (xO x) + 0)%Z + : positive -> Z +fun x : positive => (- Zpos (xO x))%Z + : positive -> Z +fun x : positive => (- Zpos (xO x) + 0)%Z + : positive -> Z +(Z_of_nat 0 + 1)%Z : Z -`0+(inject_nat (plus (0) (0)))` +(0 + Z_of_nat (0 + 0))%Z : Z -`(inject_nat (0)) = 0` +Z_of_nat 0 = 0%Z : Prop -`0+(inject_nat (11))` +(0 + Z_of_nat 11)%Z : Z diff --git a/test-suite/output/ZSyntax.out8 b/test-suite/output/ZSyntax.out8 deleted file mode 100644 index cbfb9f207..000000000 --- a/test-suite/output/ZSyntax.out8 +++ /dev/null @@ -1,26 +0,0 @@ -32%Z - : Z -fun f : nat -> Z => (f 0%nat + 0)%Z - : (nat -> Z) -> Z -fun x : positive => Zpos (xO x) - : positive -> Z -fun x : positive => (Zpos x + 1)%Z - : positive -> Z -fun x : positive => Zpos x - : positive -> Z -fun x : positive => Zneg (xO x) - : positive -> Z -fun x : positive => (Zpos (xO x) + 0)%Z - : positive -> Z -fun x : positive => (- Zpos (xO x))%Z - : positive -> Z -fun x : positive => (- Zpos (xO x) + 0)%Z - : positive -> Z -(Z_of_nat 0 + 1)%Z - : Z -(0 + Z_of_nat (0 + 0))%Z - : Z -Z_of_nat 0 = 0%Z - : Prop -(0 + Z_of_nat 11)%Z - : Z diff --git a/test-suite/output/ZSyntax.v b/test-suite/output/ZSyntax.v index 49442b757..289a1e3f4 100644 --- a/test-suite/output/ZSyntax.v +++ b/test-suite/output/ZSyntax.v @@ -1,17 +1,17 @@ -Require ZArith. -Check `32`. -Check [f:nat->Z]`(f O) + 0`. -Check [x:positive]`(POS (xO x))`. -Check [x:positive]`(POS x)+1`. -Check [x:positive]`(POS x)`. -Check [x:positive]`(NEG (xO x))`. -Check [x:positive]`(POS (xO x))+0`. -Check [x:positive]`(Zopp (POS (xO x)))`. -Check [x:positive]`(Zopp (POS (xO x)))+0`. -Check `(inject_nat O)+1`. -Check (Zplus `0` (inject_nat (plus O O))). -Check `(inject_nat O)=0`. +Require Import ZArith. +Check 32%Z. +Check (fun f : nat -> Z => (f 0%nat + 0)%Z). +Check (fun x : positive => Zpos (xO x)). +Check (fun x : positive => (Zpos x + 1)%Z). +Check (fun x : positive => Zpos x). +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). (* Submitted by Pierre Casteran *) -Require Arith. -Check (Zplus `0` (inject_nat (11))). +Require Import Arith. +Check (0 + Z_of_nat 11)%Z. diff --git a/test-suite/output/ZSyntax.v8 b/test-suite/output/ZSyntax.v8 deleted file mode 100644 index 0412f6d68..000000000 --- a/test-suite/output/ZSyntax.v8 +++ /dev/null @@ -1,17 +0,0 @@ -Require Import ZArith. -Check 32%Z. -Check (fun f : nat -> Z => (f 0%nat + 0)%Z). -Check (fun x : positive => Zpos (xO x)). -Check (fun x : positive => (Zpos x + 1)%Z). -Check (fun x : positive => Zpos x). -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). - -(* Submitted by Pierre Casteran *) -Require Import Arith. -Check (0 + Z_of_nat 11)%Z.
\ No newline at end of file |