X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Flibrary%2FcoercDb.ml;h=c8be370f222e3cffc5f47caaecd8aef9d4875aaf;hb=6b0a195b180e3526af7b55771b2df7b10acd7c30;hp=312c2f1e49adb612332d6e0a1ddbcfa5923a8065;hpb=4ef0546be6fdf068e5a59951aa42895bebc0fa3a;p=helm.git

diff --git a/helm/software/components/library/coercDb.ml b/helm/software/components/library/coercDb.ml
index 312c2f1e4..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
@@ -166,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;
+;;