From cd4e16d545b0ca42c37e2f79f63e6c25c6ad4480 Mon Sep 17 00:00:00 2001
From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Mon, 12 Sep 2005 16:09:07 +0000
Subject: [PATCH] removed work-arounds for poor disambiguation, which should
 now be fixed with the multiple passes support ...

---
 helm/matita/library/Z/compare.ma         | 12 ++++--------
 helm/matita/library/Z/orders.ma          | 12 ++++--------
 helm/matita/library/logic/connectives.ma |  6 ------
 helm/matita/library/logic/equality.ma    |  3 ---
 4 files changed, 8 insertions(+), 25 deletions(-)

diff --git a/helm/matita/library/Z/compare.ma b/helm/matita/library/Z/compare.ma
index d2e075d26..551bfcf8a 100644
--- a/helm/matita/library/Z/compare.ma
+++ b/helm/matita/library/Z/compare.ma
@@ -106,16 +106,14 @@ simplify.exact I.
 simplify.exact I.
 elim y. simplify.exact I.
 simplify. 
-(*CSC: qui uso le perche' altrimenti ci sono troppe scelte
-  per via delle coercions! *)
 cut match (nat_compare n1 n) with
 [ LT \Rightarrow n1<n
 | EQ \Rightarrow n1=n
 | GT \Rightarrow n<n1] \to 
 match (nat_compare n1 n) with
-[ LT \Rightarrow (le (S n1) n)
+[ LT \Rightarrow (S n1) \leq n
 | EQ \Rightarrow neg n = neg n1
-| GT \Rightarrow (le (S n) n1)]. 
+| GT \Rightarrow (S n) \leq n1]. 
 apply Hcut. apply nat_compare_to_Prop. 
 elim (nat_compare n1 n).
 simplify.exact H.
@@ -125,16 +123,14 @@ simplify.exact I.
 elim y.simplify.exact I.
 simplify.exact I.
 simplify.
-(*CSC: qui uso le perche' altrimenti ci sono troppe scelte
-  per via delle coercions! *)
 cut match (nat_compare n n1) with
 [ LT \Rightarrow n<n1
 | EQ \Rightarrow n=n1
 | GT \Rightarrow n1<n] \to 
 match (nat_compare n n1) with
-[ LT \Rightarrow (le (S n) n1)
+[ LT \Rightarrow (S n) \leq n1
 | EQ \Rightarrow pos n = pos n1
-| GT \Rightarrow (le (S n1) n)]. 
+| GT \Rightarrow (S n1) \leq n]. 
 apply Hcut. apply nat_compare_to_Prop. 
 elim (nat_compare n n1).
 simplify.exact H.
diff --git a/helm/matita/library/Z/orders.ma b/helm/matita/library/Z/orders.ma
index bc5ffdb51..ec1d6fb52 100644
--- a/helm/matita/library/Z/orders.ma
+++ b/helm/matita/library/Z/orders.ma
@@ -73,26 +73,22 @@ qed.
 theorem irrefl_Zlt: irreflexive Z Zlt
 \def irreflexive_Zlt.
 
-(*CSC: qui uso lt perche' ho due istanze diverse di < *)
 theorem Zlt_neg_neg_to_lt: 
-\forall n,m:nat. neg n < neg m \to lt m n.
+\forall n,m:nat. neg n < neg m \to m < n.
 intros.apply H.
 qed.
 
-(*CSC: qui uso lt perche' ho due istanze diverse di < *)
-theorem lt_to_Zlt_neg_neg: \forall n,m:nat.lt m n \to neg n < neg m. 
+theorem lt_to_Zlt_neg_neg: \forall n,m:nat.m < n \to neg n < neg m. 
 intros.
 simplify.apply H.
 qed.
 
-(*CSC: qui uso lt perche' ho due istanze diverse di < *)
 theorem Zlt_pos_pos_to_lt: 
-\forall n,m:nat. pos n < pos m \to lt n m.
+\forall n,m:nat. pos n < pos m \to n < m.
 intros.apply H.
 qed.
 
-(*CSC: qui uso lt perche' ho due istanze diverse di < *)
-theorem lt_to_Zlt_pos_pos: \forall n,m:nat.lt n m \to pos n < pos m. 
+theorem lt_to_Zlt_pos_pos: \forall n,m:nat.n < m \to pos n < pos m. 
 intros.
 simplify.apply H.
 qed.
diff --git a/helm/matita/library/logic/connectives.ma b/helm/matita/library/logic/connectives.ma
index dacf542af..057bed878 100644
--- a/helm/matita/library/logic/connectives.ma
+++ b/helm/matita/library/logic/connectives.ma
@@ -28,8 +28,6 @@ definition Not: Prop \to Prop \def
 
 (*CSC: the URI must disappear: there is a bug now *)
 interpretation "logical not" 'not x = (cic:/matita/logic/connectives/Not.con x).
-(*CSC: this alias should disappear. It is now required because the notation for Coq is pre-loaded *)
-alias symbol "not" (instance 0) = "logical not".
 
 theorem absurd : \forall A,C:Prop. A \to \lnot A \to C.
 intros. elim (H1 H).
@@ -42,8 +40,6 @@ inductive And (A,B:Prop) : Prop \def
 
 (*CSC: the URI must disappear: there is a bug now *)
 interpretation "logical and" 'and x y = (cic:/matita/logic/connectives/And.ind#xpointer(1/1) x y).
-(*CSC: this alias should disappear. It is now required because the notation for Coq is pre-loaded *)
-alias symbol "and" (instance 0) = "logical and".
 
 theorem proj1: \forall A,B:Prop. A \land B \to A.
 intros. elim H. assumption.
@@ -59,8 +55,6 @@ inductive Or (A,B:Prop) : Prop \def
 
 (*CSC: the URI must disappear: there is a bug now *)
 interpretation "logical or" 'or x y = (cic:/matita/logic/connectives/Or.ind#xpointer(1/1) x y).
-(*CSC: this alias should disappear. It is now required because the notation for Coq is pre-loaded *)
-alias symbol "or" (instance 0) = "logical or".
    
 definition decidable : Prop \to Prop \def \lambda A:Prop. A \lor \not A.
 
diff --git a/helm/matita/library/logic/equality.ma b/helm/matita/library/logic/equality.ma
index 77ef0eb82..a561827f8 100644
--- a/helm/matita/library/logic/equality.ma
+++ b/helm/matita/library/logic/equality.ma
@@ -22,10 +22,7 @@ inductive eq (A:Type) (x:A) : A \to Prop \def
 (*CSC: the URI must disappear: there is a bug now *)
 interpretation "leibnitz's equality"
    'eq x y = (cic:/matita/logic/equality/eq.ind#xpointer(1/1) _ x y).
-(*CSC: this alias should disappear. It is now required because the notation for Coq is pre-loaded *)
-alias symbol "eq" (instance 0) = "leibnitz's equality".
 
-    
 theorem reflexive_eq : \forall A:Type. reflexive A (eq A).
 simplify.intros.apply refl_eq.
 qed.
-- 
2.39.2