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
| 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
;;
-let to_list () =
- List.map (fun (s,t,l) -> s,t,List.map (fun a,_,b,c -> a,b,c) l) !db
+let to_list db =
+ List.map (fun (s,t,l) -> s,t,List.map (fun a,_,b,c -> a,b,c) l) db
;;
let rec myfilter p = function
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;
+;;