From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 26 Sep 2006 08:48:08 +0000 (+0000)
Subject: discriminate => destruct
X-Git-Tag: make_still_working~6858
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=88d9b90eb45721abe07bfce2c4d0768ef6420443;p=helm.git

discriminate => destruct
---

diff --git a/helm/software/matita/tests/decl.ma b/helm/software/matita/tests/decl.ma
index a0d3a0bd6..138e37e71 100644
--- a/helm/software/matita/tests/decl.ma
+++ b/helm/software/matita/tests/decl.ma
@@ -200,7 +200,7 @@ theorem easy6: ∀t. O ≮ O → O < size t → t ≠ Empty.
      suppose (Node t1 t2 = Empty) (absurd).
      (* Discriminate should really generate a theorem to be useful with
         declarative tactics *)
-     discriminate absurd.
+     destruct absurd.
      by final
    done.
 qed.
\ No newline at end of file