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

5 files changed, 40 insertions, 41 deletions

diff --git a/library/decl_kinds.ml b/library/decl_kinds.ml
index 0e2ef95739..6eb582baef 100644
--- a/library/decl_kinds.ml
+++ b/library/decl_kinds.ml
@@ -10,16 +10,8 @@
 
 (** Informal mathematical status of declarations *)
 
-type discharge = DoDischarge | NoDischarge
-
-type import_status = ImportDefaultBehavior | ImportNeedQualified
-
-type locality = Discharge | Global of import_status
-
 type binding_kind = Explicit | Implicit
 
-type polymorphic = bool
-
 type private_flag = bool
 
 type cumulative_inductive_flag = bool
@@ -58,17 +50,12 @@ type assumption_object_kind = Definitional | Logical | Conjectural | Context
    Logical      |  Hypothesis | Axiom
 
 *)
-type assumption_kind = locality * polymorphic * assumption_object_kind
-type definition_kind = locality * polymorphic * definition_object_kind
-
 (** Kinds used in proofs *)
 
 type goal_object_kind =
   | DefinitionBody of definition_object_kind
   | Proof of theorem_kind
 
-type goal_kind = locality * polymorphic * goal_object_kind
-
 (** Kinds used in library *)
 
 type logical_kind =
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
diff --git a/library/decls.mli b/library/decls.mli
index 0d09499b51..f88958bb04 100644
--- a/library/decls.mli
+++ b/library/decls.mli
@@ -18,8 +18,13 @@ open Decl_kinds
 
 (** Registration and access to the table of variable *)
 
-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;
+}
 
 val add_variable_data : variable -> variable_data -> unit
 val variable_path : variable -> DirPath.t
@@ -27,7 +32,7 @@ val variable_secpath : variable -> qualid
 val variable_kind : variable -> logical_kind
 val variable_opacity : variable -> bool
 val variable_context : variable -> Univ.ContextSet.t
-val variable_polymorphic : variable -> polymorphic
+val variable_polymorphic : variable -> bool
 val variable_exists : variable -> bool
 
 (** Registration and access to the table of constants *)
diff --git a/library/lib.ml b/library/lib.ml
index ae657dbd70..3eb74808e4 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -411,8 +411,12 @@ type abstr_info = {
 type abstr_list = abstr_info Names.Cmap.t * abstr_info Names.Mindmap.t
 
 type secentry =
-  | Variable of (Names.Id.t * Decl_kinds.binding_kind *
-		   Decl_kinds.polymorphic * Univ.ContextSet.t)
+  | Variable of {
+      id:Names.Id.t;
+      kind:Decl_kinds.binding_kind;
+      poly:bool;
+      univs:Univ.ContextSet.t;
+    }
   | Context of Univ.ContextSet.t
 
 let sectab =
@@ -424,16 +428,16 @@ let add_section () =
                 (Names.Cmap.empty,Names.Mindmap.empty)) :: !sectab
 
 let check_same_poly p vars =
-  let pred = function Context _ -> p = false | Variable (_, _, poly, _) -> p != poly in
+  let pred = function Context _ -> p = false | Variable {poly} -> p != poly in
   if List.exists pred vars then
     user_err Pp.(str  "Cannot mix universe polymorphic and monomorphic declarations in sections.")
 
-let add_section_variable id impl poly ctx =
+let add_section_variable ~name ~kind ~poly univs =
   match !sectab with
     | [] -> () (* because (Co-)Fixpoint temporarily uses local vars *)
     | (vars,repl,abs)::sl ->
        List.iter (fun tab -> check_same_poly poly (pi1 tab)) !sectab;
-       sectab := (Variable (id,impl,poly,ctx)::vars,repl,abs)::sl
+       sectab := (Variable {id=name;kind;poly;univs}::vars,repl,abs)::sl
 
 let add_section_context ctx =
   match !sectab with
@@ -448,7 +452,7 @@ let is_polymorphic_univ u =
     let open Univ in
     List.iter (fun (vars,_,_) ->
         List.iter (function
-            | Variable (_,_,poly,(univs,_)) ->
+            | Variable {poly;univs=(univs,_)} ->
               if LSet.mem u univs then raise (PolyFound poly)
             | Context (univs,_) ->
               if LSet.mem u univs then raise (PolyFound true)
@@ -459,12 +463,12 @@ let is_polymorphic_univ u =
 
 let extract_hyps (secs,ohyps) =
   let rec aux = function
-    | (Variable (id,impl,poly,ctx)::idl, decl::hyps) when Names.Id.equal id (NamedDecl.get_id decl) ->
+    | (Variable {id;kind;poly;univs}::idl, decl::hyps) when Names.Id.equal id (NamedDecl.get_id decl) ->
       let l, r = aux (idl,hyps) in 
-      (decl,impl) :: l, if poly then Univ.ContextSet.union r ctx else r
-    | (Variable (_,_,poly,ctx)::idl,hyps) ->
+      (decl,kind) :: l, if poly then Univ.ContextSet.union r univs else r
+    | (Variable {poly;univs}::idl,hyps) ->
         let l, r = aux (idl,hyps) in
-          l, if poly then Univ.ContextSet.union r ctx else r
+          l, if poly then Univ.ContextSet.union r univs else r
     | (Context ctx :: idl, hyps) ->
        let l, r = aux (idl, hyps) in
        l, Univ.ContextSet.union r ctx
@@ -509,11 +513,11 @@ let add_section_replacement f g poly hyps =
     } in
     sectab := (vars,f (inst,args) exps, g info abs) :: sl
 
-let add_section_kn poly kn =
+let add_section_kn ~poly kn =
   let f x (l1,l2) = (l1,Names.Mindmap.add kn x l2) in
     add_section_replacement f f poly
 
-let add_section_constant poly kn =
+let add_section_constant ~poly kn =
   let f x (l1,l2) = (Names.Cmap.add kn x l1,l2) in
     add_section_replacement f f poly
 
@@ -543,7 +547,7 @@ let variable_section_segment_of_reference gr =
 let section_instance = function
   | VarRef id ->
      let eq = function
-       | Variable (id',_,_,_) -> Names.Id.equal id id'
+       | Variable {id=id'} -> Names.Id.equal id id'
        | Context _ -> false
      in
      if List.exists eq (pi1 (List.hd !sectab))
diff --git a/library/lib.mli b/library/lib.mli
index f6bd61e2da..2cd43b66b3 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -178,12 +178,10 @@ val variable_section_segment_of_reference : GlobRef.t -> variable_context
 val section_instance : GlobRef.t -> Univ.Instance.t * Id.t array
 val is_in_section : GlobRef.t -> bool
 
-val add_section_variable : Id.t -> Decl_kinds.binding_kind -> Decl_kinds.polymorphic -> Univ.ContextSet.t -> unit
+val add_section_variable : name:Id.t -> kind:Decl_kinds.binding_kind -> poly:bool -> Univ.ContextSet.t -> unit
 val add_section_context : Univ.ContextSet.t -> unit
-val add_section_constant : Decl_kinds.polymorphic ->
-  Constant.t -> Constr.named_context -> unit
-val add_section_kn : Decl_kinds.polymorphic ->
-  MutInd.t -> Constr.named_context -> unit
+val add_section_constant : poly:bool -> Constant.t -> Constr.named_context -> unit
+val add_section_kn : poly:bool -> MutInd.t -> Constr.named_context -> unit
 val replacement_context : unit -> Opaqueproof.work_list
 
 val is_polymorphic_univ : Univ.Level.t -> bool