2 files changed, 12 insertions, 0 deletions
diff --git a/test-suite/output/Tactics.out b/test-suite/output/Tactics.out
index 71c59e4327..8e8b8059f9 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 24a33651cd..8fa9199408 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.