evd/evarutil: safe [add_unification_pb] interface, taking EConstr's

Avoid adding the same unification problem twice, module evar instantiation.

1 files changed, 2 insertions, 1 deletions

diff --git a/engine/evd.ml b/engine/evd.ml
index 0c9c3a29b2..2226193cb5 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -621,10 +621,11 @@ let set_universe_context evd uctx' =
   { evd with universes = uctx' }
 
 let add_conv_pb ?(tail=false) pb d =
-  (** MS: we have duplicates here, why? *)
   if tail then {d with conv_pbs = d.conv_pbs @ [pb]}
   else {d with conv_pbs = pb::d.conv_pbs}
 
+let conv_pbs d = d.conv_pbs
+
 let evar_source evk d = (find d evk).evar_source
 
 let evar_ident evk evd = EvNames.ident evk evd.evar_names