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/evarutil.mli | 8 ++++++++ 1 file changed, 8 insertions(+) (limited to 'engine/evarutil.mli') diff --git a/engine/evarutil.mli b/engine/evarutil.mli index c17f3d168..db638be9e 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 *) -- cgit v1.2.3