summaryrefslogtreecommitdiff
path: root/test-suite/output
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/output')
-rw-r--r--test-suite/output/Cases.out21
-rw-r--r--test-suite/output/Cases.v29
-rw-r--r--test-suite/output/Fixpoint.out14
-rw-r--r--test-suite/output/Fixpoint.v23
-rw-r--r--test-suite/output/Implicit.out5
-rw-r--r--test-suite/output/Implicit.v19
-rw-r--r--test-suite/output/InitSyntax.out3
-rw-r--r--test-suite/output/Nametab.out36
-rw-r--r--test-suite/output/Nametab.v22
-rw-r--r--test-suite/output/Notations.out4
-rw-r--r--test-suite/output/Notations.v10
-rw-r--r--test-suite/output/Tactics.out2
-rw-r--r--test-suite/output/TranspModtype.out3
-rw-r--r--test-suite/output/ZSyntax.out10
-rw-r--r--test-suite/output/reduction.out4
-rw-r--r--test-suite/output/reduction.v13
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.
+
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-02 06:24:54 +0000