- match (decontextualize [] x) with
- | ctx, NCic.Appl [_;_;a;b] -> index_hint empty_db ctx a b
- | _ -> assert false
- with exn -> prerr_endline ("PIPPO" ^ Printexc.to_string exn); empty_db
-
-(* List.fold_left
- (fun db (_,tgt,clist) ->
- List.fold_left
- (fun db (uri,_,arg) ->
- let c=fst (OCic2NCic.convert_term uri (CicUtil.term_of_uri uri)) in
- let arity = match tgt with | CoercDb.Fun i -> i | _ -> 0 in
- let src, tgt =
- let cty = NCicTypeChecker.typeof ~subst:[] ~metasenv:[] [] c in
- let scty, metasenv,_ =
- NCicMetaSubst.saturate ~delta:max_int [] [] [] cty (arity+1)
- in
- match scty with
- | NCic.Prod (_, src, tgt) ->
- let tgt =
- NCicSubstitution.subst (NCic.Meta (-1,(0,NCic.Irl 0))) tgt
- in
+ let mk_hint (u1,_,_) (u2,_,_) =
+ let l = OCic2NCic.convert_obj u1
+ (fst (CicEnvironment.get_obj CicUniv.oblivion_ugraph u1)) in
+ let r = OCic2NCic.convert_obj u2
+ (fst (CicEnvironment.get_obj CicUniv.oblivion_ugraph u2)) in
+ match List.hd l,List.hd r with
+ | (_,_,_,_,NCic.Constant (_,_,Some l,_,_)),
+ (_,_,_,_,NCic.Constant (_,_,Some r,_,_)) ->
+ let rec aux ctx t1 t2 =
+ match t1, t2 with
+ | NCic.Lambda (n1,s1,b1), NCic.Lambda(_,s2,b2) ->
+ if NCicReduction.are_convertible ~subst:[] ~metasenv:[] ctx s1 s2
+ then aux ((n1, NCic.Decl s1) :: ctx) b1 b2
+ else None
+ | b1,b2 ->
+ if NCicReduction.are_convertible ~subst:[] ~metasenv:[] ctx b1 b2
+ then begin