(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)