From 36b78e4e0fccc476015d9c34c23f47df4ae5c6e0 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 24 Apr 2006 10:23:30 +0000
Subject: Timide tentative de clarification du statut de l'opérateur de
 filtrage PCase dans le type pattern: le type pattern est utilisé
 essentiellement dans ltac, il est normalement obtenu sans typage, et ce via
 rawconstr (sauf cas de filtrage ltac non linéaire où il est obtenu de
 constr). Le cas d'un filtrage sur un "if" doit être traité à part car sans le
 type, il est impossible de savoir le nombre d'arguments du constructeur
 puisque par définition du "if", ceux-ci ne sont pas liants et ne laissent pas
 dans la syntaxe concrète (résolution au passage du bug #1070, dû à un
 filtrage incomplet dans le passage de pattern à rawconstr permettant
 l'affichage des pattern).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8728 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 test-suite/output/Tactics.out | 3 +++
 test-suite/output/Tactics.v   | 9 +++++++++
 2 files changed, 12 insertions(+)

(limited to 'test-suite')

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.
-- 
cgit v1.2.3