From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 19 Sep 2005 14:02:25 +0000 (+0000)
Subject: Spurious interpretation removed.
X-Git-Tag: LAST_BEFORE_NEW~96
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=2826aed999b30a6f53978fe457c1e5f3587ac6d6;p=helm.git

Spurious interpretation removed.
---

diff --git a/helm/matita/library/list/list.ma b/helm/matita/library/list/list.ma
index 417c88ee7..0b7340d05 100644
--- a/helm/matita/library/list/list.ma
+++ b/helm/matita/library/list/list.ma
@@ -16,9 +16,6 @@ set "baseuri" "cic:/matita/list/".
 include "logic/equality.ma".
 include "higher_order_defs/functions.ma".
 
-interpretation "leibnitz's equality" 'eq x y =
-  (cic:/matita/logic/equality/eq.ind#xpointer(1/1) _ x y).
-
 notation "hvbox(hd break :: tl)"
   right associative with precedence 46
   for @{'cons $hd $tl}.