From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Mon, 27 Nov 2006 12:20:35 +0000 (+0000)
Subject: Matita's default equality has changed
X-Git-Tag: 0.4.95@7852~780
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d92f4fde249a95ae38360b0ce0fcaa0bd265ad8b;p=helm.git

Matita's default equality has changed
-This line, and those below, will be ignored--

M    library/logic/equality.ma
---

diff --git a/matita/library/logic/equality.ma b/matita/library/logic/equality.ma
index 3b242c667..2dc6cb435 100644
--- a/matita/library/logic/equality.ma
+++ b/matita/library/logic/equality.ma
@@ -36,22 +36,22 @@ theorem eq_ind':
     [refl_eq \Rightarrow H]).
 qed.
  
-theorem reflexive_eq : \forall A:Type. reflexive A (eq A).
-simplify.intros.apply refl_eq.
-qed.
+variant reflexive_eq : \forall A:Type. reflexive A (eq A)
+\def refl_eq.
+(* simplify.intros.apply refl_eq. *)
     
 theorem symmetric_eq: \forall A:Type. symmetric A (eq A).
 unfold symmetric.intros.elim H. apply refl_eq.
 qed.
 
-theorem sym_eq : \forall A:Type.\forall x,y:A. x=y  \to y=x
+variant sym_eq : \forall A:Type.\forall x,y:A. x=y  \to y=x
 \def symmetric_eq.
 
 theorem transitive_eq : \forall A:Type. transitive A (eq A).
 unfold transitive.intros.elim H1.assumption.
 qed.
 
-theorem trans_eq : \forall A:Type.\forall x,y,z:A. x=y  \to y=z \to x=z
+variant trans_eq : \forall A:Type.\forall x,y,z:A. x=y  \to y=z \to x=z
 \def transitive_eq.
 
 theorem eq_elim_r:
@@ -77,8 +77,8 @@ coercion cic:/matita/logic/equality/eq_f.con.
 
 default "equality"
  cic:/matita/logic/equality/eq.ind
- cic:/matita/logic/equality/sym_eq.con
- cic:/matita/logic/equality/trans_eq.con
+ cic:/matita/logic/equality/symmetric_eq.con
+ cic:/matita/logic/equality/transitive_eq.con
  cic:/matita/logic/equality/eq_ind.con
  cic:/matita/logic/equality/eq_elim_r.con
  cic:/matita/logic/equality/eq_f.con