diff options
Diffstat (limited to 'engine/evd.ml')
| -rw-r--r-- | engine/evd.ml | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/engine/evd.ml b/engine/evd.ml index 0c9c3a29b2..714a0b645d 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 @@ -894,6 +895,9 @@ let check_eq evd s s' = let check_leq evd s s' = UGraph.check_leq (UState.ugraph evd.universes) s s' +let check_constraints evd csts = + UGraph.check_constraints csts (UState.ugraph evd.universes) + let fix_undefined_variables evd = { evd with universes = UState.fix_undefined_variables evd.universes } |