aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/decls.mli
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2016-09-22 16:57:38 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2016-09-22 16:57:38 +0200
commit3c47248abc27aa9c64120db30dcb0d7bf945bc70 (patch)
tree0dd3a804e1924862390a7f78abc9a8a119127f9c /library/decls.mli
parentceb68d1d643ac65f500e0201f61e73cf22e6e2fb (diff)
parent1bc1cba7a759a285131a3ed6ea8979716700b856 (diff)
Merge remote-tracking branch 'github/pr/283' into trunk
Was PR#283: Stylistic improvements in intf/decl_kinds.mli.
Diffstat (limited to 'library/decls.mli')
-rw-r--r--library/decls.mli6
1 files changed, 5 insertions, 1 deletions
diff --git a/library/decls.mli b/library/decls.mli
index 1ca7f8946..e84a6376b 100644
--- a/library/decls.mli
+++ b/library/decls.mli
@@ -17,7 +17,11 @@ open Decl_kinds
(** Registration and access to the table of variable *)
type variable_data =
- DirPath.t * bool (** opacity *) * Univ.universe_context_set * polymorphic * logical_kind
+ { dir_path : DirPath.t;
+ opaque : bool;
+ universe_context_set : Univ.universe_context_set;
+ polymorphic : bool;
+ kind : logical_kind }
val add_variable_data : variable -> variable_data -> unit
val variable_path : variable -> DirPath.t