Merge PR #10316: [lemmas] Reify info for implicits, universe decls, and rec theorems.

Reviewed-by: SkySkimmer
Ack-by: ejgallego
Reviewed-by: gares
Reviewed-by: ppedrot

1 files changed, 12 insertions, 7 deletions

diff --git a/library/decls.ml b/library/decls.ml
index ef60a44ac7..5cb35323dd 100644
--- a/library/decls.ml
+++ b/library/decls.ml
@@ -17,19 +17,24 @@ open Libnames
 
 (** Datas associated to section variables and local definitions *)
 
-type variable_data =
-  DirPath.t * bool (* opacity *) * Univ.ContextSet.t * polymorphic * logical_kind
+type variable_data = {
+  path:DirPath.t;
+  opaque:bool;
+  univs:Univ.ContextSet.t;
+  poly:bool;
+  kind: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 = 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_path id = let {path} = Id.Map.find id !vartab in path
+let variable_opacity id = let {opaque} = Id.Map.find id !vartab in opaque
+let variable_kind id = let {kind} = Id.Map.find id !vartab in kind
+let variable_context id = let {univs} = Id.Map.find id !vartab in univs
+let variable_polymorphic id = let {poly} = Id.Map.find id !vartab in poly
 
 let variable_secpath id =
   let dir = drop_dirpath_prefix (Lib.library_dp()) (variable_path id) in