aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker/univ.mli
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2017-07-07 16:33:47 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2017-07-11 14:50:47 +0200
commit0d9a91113c4112eece0680e433f435fdfb39ea4b (patch)
treecf90d290a92c02a2297b3a13b77190db9aa4db70 /checker/univ.mli
parentb5ad6a80107f196fa8ffcc4f5dff58bea8c4f70e (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.mli')
-rw-r--r--checker/univ.mli1
1 files changed, 1 insertions, 0 deletions
diff --git a/checker/univ.mli b/checker/univ.mli
index 457ccbdff..faa682cbf 100644
--- a/checker/univ.mli
+++ b/checker/univ.mli
@@ -209,6 +209,7 @@ sig
type t
val instance : t -> Instance.t
+ val size : t -> int
end