diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-06-23 15:52:48 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-06-23 15:52:48 +0200 |
| commit | ddd99ca6b4a23286405ec995379e4b07d42b0f78 (patch) | |
| tree | e2e328b78d9fca7383973bf46014410ea08bac4f /engine/evd.ml | |
| parent | 38b180984b09840e0b1023cc441917acc77dd438 (diff) | |
| parent | 994f869496b3edd76a903cac16b13e8b6f247d63 (diff) | |
Merge PR #7827: [engine] safe [add_unification_pb] interface
Diffstat (limited to 'engine/evd.ml')
| -rw-r--r-- | engine/evd.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/engine/evd.ml b/engine/evd.ml index f56f9662d..714a0b645 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -621,10 +621,11 @@ let set_universe_context evd uctx' = { evd with universes = uctx' } let add_conv_pb ?(tail=false) pb d = - (** MS: we have duplicates here, why? *) if tail then {d with conv_pbs = d.conv_pbs @ [pb]} else {d with conv_pbs = pb::d.conv_pbs} +let conv_pbs d = d.conv_pbs + let evar_source evk d = (find d evk).evar_source let evar_ident evk evd = EvNames.ident evk evd.evar_names |