From 4ef0546be6fdf068e5a59951aa42895bebc0fa3a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 6 Jan 2009 18:19:28 +0000 Subject: [PATCH] coercions reordering implemented --- helm/software/components/library/coercDb.ml | 10 +++++++++- helm/software/matita/dist/ChangeLog | 2 ++ 2 files changed, 11 insertions(+), 1 deletion(-) 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 -- 2.39.2