summaryrefslogtreecommitdiff
path: root/test-suite/output
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2006-06-16 14:41:51 +0000
committerGravatar Samuel Mimram <smimram@debian.org>2006-06-16 14:41:51 +0000
commite978da8c41d8a3c19a29036d9c569fbe2a4616b0 (patch)
tree0de2a907ee93c795978f3c843155bee91c11ed60 /test-suite/output
parent3ef7797ef6fc605dfafb32523261fe1b023aeecb (diff)
Imported Upstream version 8.0pl3+8.1betaupstream/8.0pl3+8.1beta
Diffstat (limited to 'test-suite/output')
-rw-r--r--test-suite/output/Cases.out2
-rw-r--r--test-suite/output/InitSyntax.out2
-rw-r--r--test-suite/output/Tactics.out3
-rw-r--r--test-suite/output/Tactics.v9
4 files changed, 14 insertions, 2 deletions
diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out
index 63137edb..a3033e94 100644
--- a/test-suite/output/Cases.out
+++ b/test-suite/output/Cases.out
@@ -2,7 +2,7 @@ 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)
+ | k _ 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/InitSyntax.out b/test-suite/output/InitSyntax.out
index 4ed72c50..c7f3ed7d 100644
--- a/test-suite/output/InitSyntax.out
+++ b/test-suite/output/InitSyntax.out
@@ -1,4 +1,4 @@
-Inductive sig2 (A : Set) (P : A -> Prop) (Q : A -> Prop) : Set :=
+Inductive sig2 (A : Type) (P : A -> Prop) (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
diff --git a/test-suite/output/Tactics.out b/test-suite/output/Tactics.out
index 71c59e43..8e8b8059 100644
--- a/test-suite/output/Tactics.out
+++ b/test-suite/output/Tactics.out
@@ -1 +1,4 @@
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/Tactics.v b/test-suite/output/Tactics.v
index 24a33651..8fa91994 100644
--- a/test-suite/output/Tactics.v
+++ b/test-suite/output/Tactics.v
@@ -7,3 +7,12 @@ Lemma test : True -> True /\ True.
intro H; split; [a H|e H].
Show Script.
Qed.
+
+(* 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.