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.ml | |
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.ml')
-rw-r--r-- | engine/evarutil.ml | 15 |
1 files changed, 15 insertions, 0 deletions
diff --git a/engine/evarutil.ml b/engine/evarutil.ml index 82be4791f..1625f6fc8 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -514,6 +514,21 @@ let e_new_evar env evdref ?(src=default_source) ?filter ?candidates ?store ?nami evdref := evd'; ev +(* Safe interface to unification problems *) +type unification_pb = conv_pb * env * EConstr.constr * EConstr.constr + +let eq_unification_pb evd (pbty,env,t1,t2) (pbty',env',t1',t2') = + pbty == pbty' && env == env' && + EConstr.eq_constr evd t1 t1' && + EConstr.eq_constr evd t2 t2' + +let add_unification_pb ?(tail=false) pb evd = + let conv_pbs = Evd.conv_pbs evd in + if not (List.exists (eq_unification_pb evd pb) conv_pbs) then + let (pbty,env,t1,t2) = pb in + Evd.add_conv_pb ~tail (pbty,env,t1,t2) evd + else evd + (* This assumes an evar with identity instance and generalizes it over only the de Bruijn part of the context *) let generalize_evar_over_rels sigma (ev,args) = |