diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-07-07 16:33:47 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-07-11 14:50:47 +0200 |
| commit | 0d9a91113c4112eece0680e433f435fdfb39ea4b (patch) | |
| tree | cf90d290a92c02a2297b3a13b77190db9aa4db70 /checker/univ.ml | |
| parent | b5ad6a80107f196fa8ffcc4f5dff58bea8c4f70e (diff) | |
Getting rid of simple calls to AUContext.instance.
This function breaks the abstraction barrier of abstract universe contexts,
as it provides a way to observe the bound names of such a context. We remove
all the uses that can be easily get rid of with the current API.
Diffstat (limited to 'checker/univ.ml')
| -rw-r--r-- | checker/univ.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/checker/univ.ml b/checker/univ.ml index b434db129..4eebcb25b 100644 --- a/checker/univ.ml +++ b/checker/univ.ml @@ -1175,6 +1175,7 @@ struct let make x = x let instance (univs, cst) = univs let constraints (univs, cst) = cst + let size (univs, _) = Instance.length univs let is_empty (univs, cst) = Instance.is_empty univs && Constraint.is_empty cst let pr prl (univs, cst as ctx) = |