Imported Upstream version 8.0pl3+8.1betaupstream/8.0pl3+8.1beta

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.