diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-08-09 18:24:30 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-08-09 18:24:30 +0200 |
| commit | c5a4aba58f973898ebc9af5176753c7962bddb3c (patch) | |
| tree | ce08feb40859945ea0cf9ba9a67df23c9bb03f4a /kernel/univ.ml | |
| parent | 56a6727525e860a155b6ae73da152e558b3ea976 (diff) | |
Adding a primitive to merge ContextSets which is more efficient when one
of the argument is smaller than the other one.
Diffstat (limited to 'kernel/univ.ml')
| -rw-r--r-- | kernel/univ.ml | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/kernel/univ.ml b/kernel/univ.ml index d3201bcb9..942c90aa2 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -1876,6 +1876,11 @@ struct let union (univs, cst) (univs', cst') = LSet.union univs univs', Constraint.union cst cst' + let append (univs, cst) (univs', cst') = + let univs = LSet.fold LSet.add univs univs' in + let cst = Constraint.fold Constraint.add cst cst' in + (univs, cst) + let diff (univs, cst) (univs', cst') = LSet.diff univs univs', Constraint.diff cst cst' |