From 994f869496b3edd76a903cac16b13e8b6f247d63 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 24 Jul 2017 15:09:33 +0200
Subject: evd/evarutil: safe [add_unification_pb] interface, taking EConstr's

Avoid adding the same unification problem twice, module evar instantiation.
---
 engine/evd.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'engine/evd.ml')

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
-- 
cgit v1.2.3