(Printf.sprintf "OK: %s" (CicPp.ppterm term)));
let o = !Utils.compare_terms t1 t2 in
let stat = (ty,t1,t2,o) in
-(* let w = compute_equality_weight stat in *)
- let w = 0 in
+ (* let w = compute_equality_weight stat in *)
+ let w = 0 in
let proof = Equality.Exact p in
let e = Equality.mk_equality (w, proof, stat, newmetas) in
Some e, (newmeta+1)