- (fun (_,t,ul) -> List.map (fun u -> src,[uri; u],t) ul) c_from_tgt) @
+ (fun (_,t,ul) ->
+ if CoercDb.eq_carr ~exact:true src t then [] else
+ List.map (fun u -> src,[uri; u],t) ul) c_from_tgt) @
- (fun (s,_,ul) -> List.map (fun u -> s,[u; uri],tgt) ul) c_to_src) @
+ (fun (s,_,ul) ->
+ if CoercDb.eq_carr ~exact:true s tgt then [] else
+ List.map (fun u -> s,[u; uri],tgt) ul) c_to_src) @
(* generate_composite (c2 (c1 s)) in the universe graph univ
* both living in the same context and metasenv *)
let generate_composite c1 c2 context metasenv univ arity last_lam_with_inn_arg =
(* generate_composite (c2 (c1 s)) in the universe graph univ
* both living in the same context and metasenv *)
let generate_composite c1 c2 context metasenv univ arity last_lam_with_inn_arg =
let c1_ty,univ = CicTypeChecker.type_of_aux' metasenv context c1 univ in
let c2_ty,univ = CicTypeChecker.type_of_aux' metasenv context c2 univ in
let rec mk_implicits = function
let c1_ty,univ = CicTypeChecker.type_of_aux' metasenv context c1 univ in
let c2_ty,univ = CicTypeChecker.type_of_aux' metasenv context c2 univ in
let rec mk_implicits = function
(Cic.Appl ( CicSubstitution.lift 1 c2 :: mk_implicits nc2 @
[ Cic.Appl ( CicSubstitution.lift 1 c1 :: mk_implicits nc1 @
[if last_lam_with_inn_arg then Cic.Rel 1 else Cic.Implicit None])
(Cic.Appl ( CicSubstitution.lift 1 c2 :: mk_implicits nc2 @
[ Cic.Appl ( CicSubstitution.lift 1 c1 :: mk_implicits nc1 @
[if last_lam_with_inn_arg then Cic.Rel 1 else Cic.Implicit None])
List.sort
(fun (i,ctx1,ty1) (j,ctx1,ty1) ->
try List.assoc i meta2no - List.assoc j meta2no
List.sort
(fun (i,ctx1,ty1) (j,ctx1,ty1) ->
try List.assoc i meta2no - List.assoc j meta2no
let subst = create_subst_from_metas_to_rels spline_len body_metasenv in
debug_print (lazy("SUBST: "^CicMetaSubst.ppsubst body_metasenv subst));
let term = CicMetaSubst.apply_subst subst term in
let subst = create_subst_from_metas_to_rels spline_len body_metasenv in
debug_print (lazy("SUBST: "^CicMetaSubst.ppsubst body_metasenv subst));
let term = CicMetaSubst.apply_subst subst term in
debug_print (lazy ("COMPOSED SUBSTITUTED: " ^ CicPp.ppterm term));
let term, ty, metasenv, ugraph =
CicRefine.type_of_aux' metasenv context term ugraph
debug_print (lazy ("COMPOSED SUBSTITUTED: " ^ CicPp.ppterm term));
let term, ty, metasenv, ugraph =
CicRefine.type_of_aux' metasenv context term ugraph
let body_metasenv, lambdas_metasenv =
split_metasenv metasenv (spline_len + List.length context)
in
let body_metasenv, lambdas_metasenv =
split_metasenv metasenv (spline_len + List.length context)
in
debug_print (lazy ("COMPOSED: " ^ CicPp.ppterm term));
debug_print(lazy("MENV: "^CicMetaSubst.ppmetasenv [] metasenv));
term, metasenv, ugraph
debug_print (lazy ("COMPOSED: " ^ CicPp.ppterm term));
debug_print(lazy("MENV: "^CicMetaSubst.ppmetasenv [] metasenv));
term, metasenv, ugraph
- let _ = Http_getter.resolve' ~writable:true uri in
- if Http_getter.exists' uri then retry () else uri
+ let _ = Http_getter.resolve' ~local:true ~writable:true uri in
+ if Http_getter.exists' ~local:true uri then retry () else uri