(Printf.sprintf "OK: %s" (CicPp.ppterm term)));
let o = !Utils.compare_terms t1 t2 in
let stat = (ty,t1,t2,o) in
(Printf.sprintf "OK: %s" (CicPp.ppterm term)));
let o = !Utils.compare_terms t1 t2 in
let stat = (ty,t1,t2,o) in
let proof = Equality.Exact p in
let e = Equality.mk_equality (w, proof, stat, newmetas) in
Some e, (newmeta+1)
let proof = Equality.Exact p in
let e = Equality.mk_equality (w, proof, stat, newmetas) in
Some e, (newmeta+1)
let t = CicUtil.term_of_uri u in
let ty, _ = CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph in
let t = CicUtil.term_of_uri u in
let ty, _ = CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph in