From 296fe375cefc6d3a9008201c235c3d73d5cbb049 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 15 Mar 2008 11:27:24 +0000
Subject: Backtrack sur le test censé discriminer entre une erreur d'evar non
 résolue et une anomalie. Il ne marche pas. La question de trouver la bonne
 manière de tester qu'un exemple renvoie une erreur (non rattrapable par
 tactique) et une anomalie reste ouverte.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10675 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 test-suite/success/unification.v | 7 -------
 1 file changed, 7 deletions(-)

diff --git a/test-suite/success/unification.v b/test-suite/success/unification.v
index 9de78b138b..e31d67d8cd 100644
--- a/test-suite/success/unification.v
+++ b/test-suite/success/unification.v
@@ -109,10 +109,3 @@ intros.
 apply H0. (* Check that equation ?n[H] = ?n[H] is correctly considered true *)
 reflexivity.
 Qed.
-
-(* An example that failed at some time in early 2008 *)
-(* The "fun t => match ..." used to raise an anomaly instead of an error *)
-
-Ltac f := set (x:=fun t => match t with (f,_) => f 0 end).
-Goal True.
-try f. (* if an error, it is caught *)
-- 
cgit v1.2.3