discriminate => destruct

[helm.git] / helm / software / matita / tests / decl.ma

diff --git a/helm/software/matita/tests/decl.ma b/helm/software/matita/tests/decl.ma
index a0d3a0bd610f62962e0ffb73ea4d718985f49a21..138e37e71fbbd941ad9c48559796071d5d7d0135 100644 (file)
--- 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