diff options
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) = |