diff options
author | Matthieu Sozeau <mattam@mattam.org> | 2017-07-24 15:09:33 +0200 |
---|---|---|
committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2018-06-15 11:56:52 +0200 |
commit | 994f869496b3edd76a903cac16b13e8b6f247d63 (patch) | |
tree | b2bf14d15f2faf8df7a5c6a81be7e55c76248982 /engine/evarutil.mli | |
parent | 31e13998542941040343cb81787a1d7c865d5b65 (diff) |
evd/evarutil: safe [add_unification_pb] interface, taking EConstr's
Avoid adding the same unification problem twice, module evar instantiation.
Diffstat (limited to 'engine/evarutil.mli')
-rw-r--r-- | engine/evarutil.mli | 8 |
1 files changed, 8 insertions, 0 deletions
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 *) |