X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Flibrary%2FcoercDb.ml;h=c8be370f222e3cffc5f47caaecd8aef9d4875aaf;hb=460e778b47270838f98f5efd65518c1a31c96e92;hp=50db7a3c1868817d70b7e6464ef6b4da2f9b0dcd;hpb=910c252965fe17d6b5af92e4658e7d02bac82d58;p=helm.git

diff --git a/helm/software/components/library/coercDb.ml b/helm/software/components/library/coercDb.ml
index 50db7a3c1..c8be370f2 100644
--- a/helm/software/components/library/coercDb.ml
+++ b/helm/software/components/library/coercDb.ml
@@ -50,6 +50,7 @@ type coerc_db = (* coercion_entry grouped by carrier with molteplicity *)
 let db =  ref ([] : coerc_db)
 let dump () = !db 
 let restore coerc_db = db := coerc_db
+let empty_coerc_db = []
 
 let rec coerc_carr_of_term t a =
  try
@@ -78,8 +79,7 @@ let eq_carr ?(exact=false) src tgt =
       | Cic.Prod _, true -> false
       | Cic.Prod _, false -> coarse_eq
       | _ -> coarse_eq) 
-  | Sort (Cic.Type _), Sort (Cic.Type _) -> true
-  | Sort src, Sort tgt when src = tgt -> true
+  | Sort _, Sort _ -> true
   | Fun _,Fun _ when not exact -> true (* only one Funclass *)
   | Fun i,Fun j when i = j -> true (* only one Funclass *)
   | _, _ -> false
@@ -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 *)
@@ -158,3 +166,10 @@ let add_coercion (src,tgt,u,saturations,cpos) =
         db := (src,tgt,(u,1,saturations,cpos)::l)::tl @ rest
 ;;
 
+let prefer u = 
+  let prefer (s,t,l) =
+    let lb,la = List.partition (fun (uri,_,_,_) -> UriManager.eq uri u) l in
+    s,t,lb@la
+  in
+  db := List.map prefer !db;
+;;