try
match t with
| Cic.Sort s -> Sort s
- | Cic.Prod _ -> assert false
+ | Cic.Prod _ -> Fun 0
+ (* BUG: this should be the real arity. The computation
+ requires menv, context etc.., but since carrs are compared discharging Fun
+ arity... it works *)
| Cic.Appl (t::_)
| t -> Uri (CicUtil.uri_of_term t)
with Invalid_argument _ ->
match src, tgt with
| Uri src, Uri tgt ->
let coarse_eq = UriManager.eq src tgt in
- let src_noxpointer = UriManager.strip_xpointer src in
- if exact && coarse_eq && UriManager.uri_is_ind src_noxpointer then
- match
- fst (CicEnvironment.get_obj CicUniv.oblivion_ugraph src_noxpointer)
- with
- | Cic.InductiveDefinition (_,[],m,_) when m = 0 -> true
- | Cic.Constant _ -> true
- | _ -> false
- else
- coarse_eq
+ let t = CicUtil.term_of_uri src in
+ let ty,_ = CicTypeChecker.type_of_aux' [] [] t CicUniv.oblivion_ugraph in
+ (match ty, exact with
+ | 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
| Term t1, Term t2 ->
if List.exists (fun (x,_,_) -> UriManager.eq u x) l then
let l' = List.map
(fun (x,n,saturations') ->
- assert (saturations=saturations');
if UriManager.eq u x then
(x,n+1,saturations)
else
db := (src,tgt,(u,1,saturations)::l)::tl @ rest
;;
+
+type coerc_db = (coerc_carr * coerc_carr * (UriManager.uri * int * int) list) list
+let dump () = !db
+let restore coerc_db = db := coerc_db