coercions reordering implemented

diff --git a/helm/software/components/library/coercDb.ml b/helm/software/components/library/coercDb.ml
index 50db7a3c1868817d70b7e6464ef6b4da2f9b0dcd..312c2f1e49adb612332d6e0a1ddbcfa5923a8065 100644 (file)
--- 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 89ba67d7872138383ee52be9e3523c57b9c37db8..804009ef5c09fb578bb7fc9505e52e4075a2353c 100644 (file)
--- 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