diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-03-15 11:27:24 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-03-15 11:27:24 +0000 |
| commit | 296fe375cefc6d3a9008201c235c3d73d5cbb049 (patch) | |
| tree | f16cb0bb19a842b44eafe53650c8d356e95bb69e /test-suite/success/unification.v | |
| parent | ac594661da831e91f8c5a1b118ce13b90a7ec85f (diff) | |
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
Diffstat (limited to 'test-suite/success/unification.v')
| -rw-r--r-- | test-suite/success/unification.v | 7 |
1 files changed, 0 insertions, 7 deletions
diff --git a/test-suite/success/unification.v b/test-suite/success/unification.v index 9de78b138..e31d67d8c 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 *) |