diff options
Diffstat (limited to 'test-suite/output')
-rw-r--r-- | test-suite/output/Cases.out | 21 | ||||
-rw-r--r-- | test-suite/output/Cases.v | 29 | ||||
-rw-r--r-- | test-suite/output/Fixpoint.out | 14 | ||||
-rw-r--r-- | test-suite/output/Fixpoint.v | 23 | ||||
-rw-r--r-- | test-suite/output/Implicit.out | 5 | ||||
-rw-r--r-- | test-suite/output/Implicit.v | 19 | ||||
-rw-r--r-- | test-suite/output/InitSyntax.out | 3 | ||||
-rw-r--r-- | test-suite/output/Nametab.out | 36 | ||||
-rw-r--r-- | test-suite/output/Nametab.v | 22 | ||||
-rw-r--r-- | test-suite/output/Notations.out | 4 | ||||
-rw-r--r-- | test-suite/output/Notations.v | 10 | ||||
-rw-r--r-- | test-suite/output/Tactics.out | 2 | ||||
-rw-r--r-- | test-suite/output/TranspModtype.out | 3 | ||||
-rw-r--r-- | test-suite/output/ZSyntax.out | 10 | ||||
-rw-r--r-- | test-suite/output/reduction.out | 4 | ||||
-rw-r--r-- | test-suite/output/reduction.v | 13 |
16 files changed, 179 insertions, 39 deletions
diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out index a3033e94..9d0d0658 100644 --- a/test-suite/output/Cases.out +++ b/test-suite/output/Cases.out @@ -6,4 +6,25 @@ fix F (t : t) : P t := end : forall P : t -> Type, (let x := t in forall x0 : x, P x0 -> P (k x0)) -> forall t : t, P t +proj = +fun (x y : nat) (P : nat -> Type) (def : P x) (prf : P y) => +match eq_nat_dec x y with +| left eqprf => + match eqprf in (_ = z) return (P z) with + | refl_equal => def + end +| right _ => prf +end + : forall (x y : nat) (P : nat -> Type), P x -> P y -> P y +Argument scopes are [nat_scope nat_scope _ _ _] +foo = +fix foo (A : Type) (l : list A) {struct l} : option A := + match l with + | nil => None (A:=A) + | x0 :: nil => Some x0 + | x0 :: (_ :: _) as l0 => foo A l0 + end + : forall A : Type, list A -> option A + +Argument scopes are [type_scope list_scope] diff --git a/test-suite/output/Cases.v b/test-suite/output/Cases.v index 452d3603..61f89d40 100644 --- a/test-suite/output/Cases.v +++ b/test-suite/output/Cases.v @@ -4,3 +4,32 @@ Inductive t : Set := k : let x := t in x -> x. Print t_rect. + +(* Do not contract nested patterns with dependent return type *) +(* see bug #1699 *) + +Require Import Arith. + +Definition proj (x y:nat) (P:nat -> Type) (def:P x) (prf:P y) : P y := + match eq_nat_dec x y return P y with + | left eqprf => + match eqprf in (_ = z) return (P z) with + | refl_equal => def + end + | _ => prf + end. + +Print proj. + +(* Use notations even below aliases *) + +Require Import List. + +Fixpoint foo (A:Type) (l:list A) : option A := + match l with + | nil => None + | x0 :: nil => Some x0 + | x0 :: (x1 :: xs) as l0 => foo A l0 + end. + +Print foo. diff --git a/test-suite/output/Fixpoint.out b/test-suite/output/Fixpoint.out index 62c9d395..f4270d3d 100644 --- a/test-suite/output/Fixpoint.out +++ b/test-suite/output/Fixpoint.out @@ -9,3 +9,17 @@ 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. + diff --git a/test-suite/output/Fixpoint.v b/test-suite/output/Fixpoint.v index fc27e8d2..2b13c204 100644 --- a/test-suite/output/Fixpoint.v +++ b/test-suite/output/Fixpoint.v @@ -16,3 +16,26 @@ Check end in f 0. +Require Import ZArith_base Omega. +Open Scope Z_scope. + +Inductive even: Z -> Prop := +| even_base: even 0 +| even_succ: forall n, odd (n - 1) -> even n +with odd: Z -> Prop := +| odd_succ: forall n, even (n - 1) -> odd n. + +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). + intros. + destruct H. + omega. + apply odd_pos_even_pos in H. + omega. + intros. + 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 38c5b827..ecfe8505 100644 --- a/test-suite/output/Implicit.out +++ b/test-suite/output/Implicit.out @@ -5,6 +5,9 @@ ex_intro (P:=fun _ : nat => True) (x:=0) I 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 _] +map id (1 :: nil) + : list nat +map id' (1 :: nil) + : list nat diff --git a/test-suite/output/Implicit.v b/test-suite/output/Implicit.v index 0ff7e87f..4c6f2b5d 100644 --- a/test-suite/output/Implicit.v +++ b/test-suite/output/Implicit.v @@ -17,3 +17,22 @@ Definition d1 y x (h : x = y :>nat) := h. Definition d2 x := d1 (y:=x). Print d2. + +(* Check maximal insertion of implicit *) + +Require Import List. + +Open Scope list_scope. + +Set Implicit Arguments. +Set Maximal Implicit Insertion. + +Definition id (A:Type) (x:A) := x. + +Check map id (1::nil). + +Definition id' (A:Type) (x:A) := x. + +Implicit Arguments id' [[A]]. + +Check map id' (1::nil). diff --git a/test-suite/output/InitSyntax.out b/test-suite/output/InitSyntax.out index c7f3ed7d..9299e010 100644 --- a/test-suite/output/InitSyntax.out +++ b/test-suite/output/InitSyntax.out @@ -1,5 +1,6 @@ -Inductive sig2 (A : Type) (P : A -> Prop) (Q : A -> Prop) : Type := +Inductive sig2 (A : Type) (P Q : A -> Prop) : Type := 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] diff --git a/test-suite/output/Nametab.out b/test-suite/output/Nametab.out index d0f15f0e..b1883ec0 100644 --- a/test-suite/output/Nametab.out +++ b/test-suite/output/Nametab.out @@ -1,12 +1,12 @@ -Constant Top.Q.N.K.id - (shorter name to refer to it in current context is Q.N.K.id) -Constant Top.Q.N.K.id - (shorter name to refer to it in current context is Q.N.K.id) -Constant Top.Q.N.K.id - (shorter name to refer to it in current context is Q.N.K.id) -Constant Top.Q.N.K.id -Constant Top.Q.N.K.id - (shorter name to refer to it in current context is Q.N.K.id) +Constant Top.Q.N.K.foo + (shorter name to refer to it in current context is Q.N.K.foo) +Constant Top.Q.N.K.foo + (shorter name to refer to it in current context is Q.N.K.foo) +Constant Top.Q.N.K.foo + (shorter name to refer to it in current context is Q.N.K.foo) +Constant Top.Q.N.K.foo +Constant Top.Q.N.K.foo + (shorter name to refer to it in current context is Q.N.K.foo) No module is referred to by basename K No module is referred to by name N.K Module Top.Q.N.K @@ -16,15 +16,15 @@ 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 in current context is K.id) -Constant Top.Q.N.K.id -Constant Top.Q.N.K.id - (shorter name to refer to it in current context is K.id) -Constant Top.Q.N.K.id - (shorter name to refer to it in current context is K.id) -Constant Top.Q.N.K.id - (shorter name to refer to it in current context is K.id) +Constant Top.Q.N.K.foo + (shorter name to refer to it in current context is K.foo) +Constant Top.Q.N.K.foo +Constant Top.Q.N.K.foo + (shorter name to refer to it in current context is K.foo) +Constant Top.Q.N.K.foo + (shorter name to refer to it in current context is K.foo) +Constant Top.Q.N.K.foo + (shorter name to refer to it in current context is K.foo) Module Top.Q.N.K No module is referred to by name N.K Module Top.Q.N.K diff --git a/test-suite/output/Nametab.v b/test-suite/output/Nametab.v index a1a7579b..357ba982 100644 --- a/test-suite/output/Nametab.v +++ b/test-suite/output/Nametab.v @@ -1,16 +1,16 @@ Module Q. Module N. Module K. - Definition id := Set. + Definition foo := Set. End K. End N. End Q. -(* Bad *) Locate id. -(* Bad *) Locate K.id. -(* Bad *) Locate N.K.id. -(* OK *) Locate Q.N.K.id. -(* OK *) Locate Top.Q.N.K.id. +(* Bad *) Locate foo. +(* Bad *) Locate K.foo. +(* Bad *) Locate N.K.foo. +(* OK *) Locate Q.N.K.foo. +(* OK *) Locate Top.Q.N.K.foo. (* Bad *) Locate Module K. (* Bad *) Locate Module N.K. @@ -28,11 +28,11 @@ End Q. Import Q.N. -(* Bad *) Locate id. -(* OK *) Locate K.id. -(* Bad *) Locate N.K.id. -(* OK *) Locate Q.N.K.id. -(* OK *) Locate Top.Q.N.K.id. +(* Bad *) Locate foo. +(* OK *) Locate K.foo. +(* Bad *) Locate N.K.foo. +(* OK *) Locate Q.N.K.foo. +(* OK *) Locate Top.Q.N.K.foo. (* OK *) Locate Module K. (* Bad *) Locate Module N.K. diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out index be4cd4fa..2066a7ef 100644 --- a/test-suite/output/Notations.out +++ b/test-suite/output/Notations.out @@ -46,3 +46,7 @@ fun x : nat => ifn x is succ n then n else 0 : bool -4 : Z +Nil + : forall A : Type, list A +NIL:list nat + : list nat diff --git a/test-suite/output/Notations.v b/test-suite/output/Notations.v index 3cc0a189..6e637aca 100644 --- a/test-suite/output/Notations.v +++ b/test-suite/output/Notations.v @@ -119,3 +119,13 @@ Require Import ZArith. Open Scope Z_scope. Notation "- 4" := (-2 + -2). Check -4. + +(**********************************************************************) +(* Check notations for references with activated or deactivated *) +(* implicit arguments *) + +Notation Nil := @nil. +Check Nil. + +Notation NIL := nil. +Check NIL : list nat. diff --git a/test-suite/output/Tactics.out b/test-suite/output/Tactics.out index 8e8b8059..287e8488 100644 --- a/test-suite/output/Tactics.out +++ b/test-suite/output/Tactics.out @@ -1,4 +1,6 @@ intro H; split; [ a H | e H ]. + intros; match goal with | |- context [if ?X then _ else _] => case X end; trivial. + diff --git a/test-suite/output/TranspModtype.out b/test-suite/output/TranspModtype.out index 41e8648b..f94ed642 100644 --- a/test-suite/output/TranspModtype.out +++ b/test-suite/output/TranspModtype.out @@ -1,10 +1,7 @@ TrM.A = M.A : Set - OpM.A = M.A : Set - TrM.B = M.B : Set - *** [ OpM.B : Set ] diff --git a/test-suite/output/ZSyntax.out b/test-suite/output/ZSyntax.out index cbfb9f20..f23198b0 100644 --- a/test-suite/output/ZSyntax.out +++ b/test-suite/output/ZSyntax.out @@ -2,19 +2,19 @@ : Z fun f : nat -> Z => (f 0%nat + 0)%Z : (nat -> Z) -> Z -fun x : positive => Zpos (xO x) +fun x : positive => Zpos x~0 : positive -> Z fun x : positive => (Zpos x + 1)%Z : positive -> Z fun x : positive => Zpos x : positive -> Z -fun x : positive => Zneg (xO x) +fun x : positive => Zneg x~0 : positive -> Z -fun x : positive => (Zpos (xO x) + 0)%Z +fun x : positive => (Zpos x~0 + 0)%Z : positive -> Z -fun x : positive => (- Zpos (xO x))%Z +fun x : positive => (- Zpos x~0)%Z : positive -> Z -fun x : positive => (- Zpos (xO x) + 0)%Z +fun x : positive => (- Zpos x~0 + 0)%Z : positive -> Z (Z_of_nat 0 + 1)%Z : Z diff --git a/test-suite/output/reduction.out b/test-suite/output/reduction.out new file mode 100644 index 00000000..ff327aa5 --- /dev/null +++ b/test-suite/output/reduction.out @@ -0,0 +1,4 @@ + = a + : nat + = n + 0 + : nat diff --git a/test-suite/output/reduction.v b/test-suite/output/reduction.v new file mode 100644 index 00000000..4a460a83 --- /dev/null +++ b/test-suite/output/reduction.v @@ -0,0 +1,13 @@ +(* Test the behaviour of hnf and simpl introduced in revision *) + +Variable n:nat. +Definition a:=0. + +Eval simpl in (fix plus (n m : nat) {struct n} : nat := + match n with + | 0 => m + | S p => S (p + m) + end) a a. + +Eval hnf in match (plus (S n) O) with S n => n | _ => O end. + |