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

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

1 files changed, 8 insertions, 0 deletions

diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index c17f3d1683..db638be9e2 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -217,6 +217,14 @@ val compare_cumulative_instances : Reduction.conv_pb -> Univ.Variance.t array ->
 val compare_constructor_instances : evar_map ->
   Univ.Instance.t -> Univ.Instance.t -> evar_map
 
+(** {6 Unification problems} *)
+type unification_pb = conv_pb * env * constr * constr
+
+(** [add_unification_pb ?tail pb sigma]
+    Add a unification problem [pb] to [sigma], if not already present.
+    Put it at the end of the list if [tail] is true, by default it is false. *)
+val add_unification_pb : ?tail:bool -> unification_pb -> evar_map -> evar_map
+
 (** {6 Removing hyps in evars'context}
 raise OccurHypInSimpleClause if the removal breaks dependencies *)