diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2016-09-22 16:57:38 +0200 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2016-09-22 16:57:38 +0200 |
commit | 3c47248abc27aa9c64120db30dcb0d7bf945bc70 (patch) | |
tree | 0dd3a804e1924862390a7f78abc9a8a119127f9c /library/decls.mli | |
parent | ceb68d1d643ac65f500e0201f61e73cf22e6e2fb (diff) | |
parent | 1bc1cba7a759a285131a3ed6ea8979716700b856 (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.mli | 6 |
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 |