select honors the substitution

[helm.git] / helm / software / components / library / coercDb.ml

diff --git a/helm/software/components/library/coercDb.ml b/helm/software/components/library/coercDb.ml
index 50db7a3c1868817d70b7e6464ef6b4da2f9b0dcd..c8be370f222e3cffc5f47caaecd8aef9d4875aaf 100644 (file)
--- 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;
+;;