From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 6 Jan 2009 18:19:28 +0000 (+0000)
Subject: coercions reordering implemented
X-Git-Tag: make_still_working~4272
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=4ef0546be6fdf068e5a59951aa42895bebc0fa3a;p=helm.git

coercions reordering implemented
---

diff --git a/helm/software/components/library/coercDb.ml b/helm/software/components/library/coercDb.ml
index 50db7a3c1..312c2f1e4 100644
--- a/helm/software/components/library/coercDb.ml
+++ b/helm/software/components/library/coercDb.ml
@@ -144,7 +144,15 @@ let add_coercion (src,tgt,u,saturations,cpos) =
   | (src,tgt,l)::tl ->
       assert (tl = []); (* not sure, this may be a feature *)
       if List.exists (fun (x,_,_,_) -> UriManager.eq u x) l then
-        let l = List.map
+        let l = 
+          let l = 
+            (* this code reorders the list so that adding an already declared 
+             * coercion moves it to the begging of the list *)
+            let item = List.find (fun (x,_,_,_) -> UriManager.eq u x) l in
+            let rest=List.filter (fun (x,_,_,_) -> not (UriManager.eq u x)) l in
+            item :: rest
+          in
+          List.map
           (fun (x,n,x_saturations,x_cpos) as e ->
             if UriManager.eq u x then
              (* not sure, this may be a feature *)
diff --git a/helm/software/matita/dist/ChangeLog b/helm/software/matita/dist/ChangeLog
index 89ba67d78..804009ef5 100644
--- a/helm/software/matita/dist/ChangeLog
+++ b/helm/software/matita/dist/ChangeLog
@@ -1,4 +1,6 @@
 0.5.7 - .../01/2009 - Pàdoa release
+	* declaring a coercion twice now makes it the first choice
+	  (reordering)
 	* UTF-8 eq classes and virtuals described in the manual and
 	  consistently printed in the TeX/UTF-8 table
 	* added a memory system for UTF-8 equivalence classes, so that