From 30a908becf31d91592a1f7934cfa3df2d67d1834 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Thu, 22 Sep 2016 17:11:12 +0200 Subject: Revert "Merge remote-tracking branch 'github/pr/283' into trunk" I hadn't realized that this PR uses OCaml's 4.03 inlined records feature. I will advocate again for a switch to the latest OCaml stable version, but meanwhile, let's revert. Sorry for the noise. This reverts commit 3c47248abc27aa9c64120db30dcb0d7bf945bc70, reversing changes made to ceb68d1d643ac65f500e0201f61e73cf22e6e2fb. --- library/decls.ml | 16 ++++++---------- 1 file changed, 6 insertions(+), 10 deletions(-) (limited to 'library/decls.ml') diff --git a/library/decls.ml b/library/decls.ml index 1e9afe968..2952c258a 100644 --- a/library/decls.ml +++ b/library/decls.ml @@ -19,22 +19,18 @@ module NamedDecl = Context.Named.Declaration (** Datas associated to section variables and local definitions *) type variable_data = - { dir_path : DirPath.t; - opaque : bool; - universe_context_set : Univ.universe_context_set; - polymorphic : bool; - kind : logical_kind } + DirPath.t * bool (* opacity *) * Univ.universe_context_set * polymorphic * logical_kind let vartab = Summary.ref (Id.Map.empty : variable_data Id.Map.t) ~name:"VARIABLE" let add_variable_data id o = vartab := Id.Map.add id o !vartab -let variable_path id = (Id.Map.find id !vartab).dir_path -let variable_opacity id = (Id.Map.find id !vartab).opaque -let variable_kind id = (Id.Map.find id !vartab).kind -let variable_context id = (Id.Map.find id !vartab).universe_context_set -let variable_polymorphic id = (Id.Map.find id !vartab).polymorphic +let variable_path id = let (p,_,_,_,_) = Id.Map.find id !vartab in p +let variable_opacity id = let (_,opaq,_,_,_) = Id.Map.find id !vartab in opaq +let variable_kind id = let (_,_,_,_,k) = Id.Map.find id !vartab in k +let variable_context id = let (_,_,ctx,_,_) = Id.Map.find id !vartab in ctx +let variable_polymorphic id = let (_,_,_,p,_) = Id.Map.find id !vartab in p let variable_secpath id = let dir = drop_dirpath_prefix (Lib.library_dp()) (variable_path id) in -- cgit v1.2.3