diff options
Diffstat (limited to 'library/decls.ml')
| -rw-r--r-- | library/decls.ml | 11 |
1 files changed, 6 insertions, 5 deletions
diff --git a/library/decls.ml b/library/decls.ml index 2d8807f80..811d09667 100644 --- a/library/decls.ml +++ b/library/decls.ml @@ -18,17 +18,18 @@ open Libnames (** Datas associated to section variables and local definitions *) type variable_data = - DirPath.t * bool (* opacity *) * Univ.constraints * 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 = 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_constraints id = let (_,_,cst,_) = Id.Map.find id !vartab in cst +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 |