-
- newmeta, (newproof, (eq_ty, left, right, ordering), newmetasenv, newargs)
+
+ let res =
+ let w = Utils.compute_equality_weight eq_ty left right in
+ (w, (eq_ty, left, right, ordering), newmetasenv, newargs)
+ in
+ Inference.store_proof res newproof;
+ newmeta, res