From 8ed6432cf793c40f69a30b1250aba7c4af31ca5f Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 9 Jun 2006 14:46:27 +0000
Subject: Adaptation Tactics.out et Cases.out au comportement actuel à défaut
 d'éviter l'affichage de trop d'espacements dans Tactics et de prendre une
 décision sur le rôle du _ dans Cases

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

diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out
index 63137edbac..a3033e94fc 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/Tactics.out b/test-suite/output/Tactics.out
index cf3a887b9f..8e8b8059f9 100644
--- a/test-suite/output/Tactics.out
+++ b/test-suite/output/Tactics.out
@@ -1,4 +1,4 @@
-intro H; split; [ a H | e H ].
+intro H; split; [  a H |  e H ].
 intros; match goal with
         | |- context [if ?X then _ else _] => case X
         end; trivial.
-- 
cgit v1.2.3