aboutsummaryrefslogtreecommitdiff
path: root/interp/decls.mli
diff options
context:
space:
mode:
authorGaëtan Gilbert2019-07-02 13:59:17 +0200
committerGaëtan Gilbert2019-07-03 17:05:29 +0200
commitbffe3e43a51420293960cc3c32845687bdee5f9b (patch)
tree8928e9137f1652552d5c394c6d040aeb888812c5 /interp/decls.mli
parent48a377680f4f3b96f7c19c22f5641877c561f03d (diff)
Remove unused Decls.variable_{context,polymorphic}
Diffstat (limited to 'interp/decls.mli')
-rw-r--r--interp/decls.mli4
1 files changed, 0 insertions, 4 deletions
diff --git a/interp/decls.mli b/interp/decls.mli
index 05e4be0de6..2a11a271cc 100644
--- a/interp/decls.mli
+++ b/interp/decls.mli
@@ -63,8 +63,6 @@ type logical_kind =
type variable_data =
{ path:DirPath.t
; opaque:bool
- ; univs:Univ.ContextSet.t
- ; poly:bool
; kind:logical_kind
}
@@ -81,6 +79,4 @@ val variable_kind : variable -> logical_kind
val variable_opacity : variable -> bool
(* Used in declare, very dubious *)
-val variable_context : variable -> Univ.ContextSet.t
-val variable_polymorphic : variable -> bool
val variable_exists : variable -> bool