aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--library/decls.ml19
-rw-r--r--library/decls.mli9
-rw-r--r--library/lib.ml26
-rw-r--r--tactics/declare.ml16
-rw-r--r--tactics/declare.mli2
-rw-r--r--vernac/comAssumption.ml28
-rw-r--r--vernac/comAssumption.mli3
-rw-r--r--vernac/lemmas.ml2
8 files changed, 60 insertions, 45 deletions
diff --git a/library/decls.ml b/library/decls.ml
index 104eb37011..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 * bool (* poly *) * 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 93298c0bc4..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 * bool (* poly *) * 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
diff --git a/library/lib.ml b/library/lib.ml
index e4054d58cc..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 * bool * Univ.ContextSet.t)
- (** (name, kind, poly, univs) *)
+ | 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 ~name ~kind ~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 (name,kind,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
@@ -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/tactics/declare.ml b/tactics/declare.ml
index 081c3a4b6a..4a4e2cf60a 100644
--- a/tactics/declare.ml
+++ b/tactics/declare.ml
@@ -264,23 +264,23 @@ let declare_definition ?(internal=UserIndividualRequest)
(** Declaration of section variables and local definitions *)
type section_variable_entry =
| SectionLocalDef of Evd.side_effects Proof_global.proof_entry
- | SectionLocalAssum of types Univ.in_universe_context_set * bool (* polymorphic *) * bool (* Implicit status *)
+ | SectionLocalAssum of { typ:types; univs:Univ.ContextSet.t; poly:bool; impl:bool }
type variable_declaration = DirPath.t * section_variable_entry * logical_kind
let cache_variable ((sp,_),o) =
match o with
| Inl ctx -> Global.push_context_set false ctx
- | Inr (id,(p,d,mk)) ->
+ | Inr (id,(path,d,kind)) ->
(* Constr raisonne sur les noms courts *)
if variable_exists id then
alreadydeclared (Id.print id ++ str " already exists");
- let impl,opaq,poly,ctx = match d with (* Fails if not well-typed *)
- | SectionLocalAssum ((ty,ctx),poly,impl) ->
- let () = Global.push_named_assum ((id,ty,poly),ctx) in
+ let impl,opaque,poly,univs = match d with (* Fails if not well-typed *)
+ | SectionLocalAssum {typ;univs;poly;impl} ->
+ let () = Global.push_named_assum ((id,typ,poly),univs) in
let impl = if impl then Implicit else Explicit in
- impl, true, poly, ctx
+ impl, true, poly, univs
| SectionLocalDef (de) ->
(* The body should already have been forced upstream because it is a
section-local definition, but it's not enforced by typing *)
@@ -307,8 +307,8 @@ let cache_variable ((sp,_),o) =
Explicit, de.proof_entry_opaque,
poly, univs in
Nametab.push (Nametab.Until 1) (restrict_path 0 sp) (VarRef id);
- add_section_variable ~name:id ~kind:impl ~poly ctx;
- add_variable_data id (p,opaq,ctx,poly,mk)
+ add_section_variable ~name:id ~kind:impl ~poly univs;
+ add_variable_data id {path;opaque;univs;poly;kind}
let discharge_variable (_,o) = match o with
| Inr (id,_) ->
diff --git a/tactics/declare.mli b/tactics/declare.mli
index 247c92bc5b..d87c096119 100644
--- a/tactics/declare.mli
+++ b/tactics/declare.mli
@@ -24,7 +24,7 @@ open Decl_kinds
type section_variable_entry =
| SectionLocalDef of Evd.side_effects Proof_global.proof_entry
- | SectionLocalAssum of types Univ.in_universe_context_set * bool (* polymorphic *) * bool (* Implicit status *)
+ | SectionLocalAssum of { typ:types; univs:Univ.ContextSet.t; poly:bool; impl:bool }
type 'a constant_entry =
| DefinitionEntry of 'a Proof_global.proof_entry
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index c098df9bef..e791118db2 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -43,15 +43,15 @@ let should_axiom_into_instance = function
true
| Definitional | Logical | Conjectural -> !axiom_into_instance
-let declare_assumption is_coe ~poly ~scope ~kind (c,ctx) pl imps impl nl {CAst.v=ident} =
+let declare_assumption is_coe ~poly ~scope ~kind typ univs pl imps impl nl {CAst.v=ident} =
let open DeclareDef in
match scope with
| Discharge ->
- let ctx = match ctx with
- | Monomorphic_entry ctx -> ctx
- | Polymorphic_entry (_, ctx) -> Univ.ContextSet.of_context ctx
+ let univs = match univs with
+ | Monomorphic_entry univs -> univs
+ | Polymorphic_entry (_, univs) -> Univ.ContextSet.of_context univs
in
- let decl = (Lib.cwd(), SectionLocalAssum ((c,ctx),poly,impl), IsAssumption kind) in
+ let decl = (Lib.cwd(), SectionLocalAssum {typ;univs;poly;impl}, IsAssumption kind) in
let _ = declare_variable ident decl in
let () = assumption_message ident in
let r = VarRef ident in
@@ -69,7 +69,7 @@ match scope with
| DefaultInline -> Some (Flags.get_inline_level())
| InlineAt i -> Some i
in
- let decl = (Declare.ParameterEntry (None,(c,ctx),inl), IsAssumption kind) in
+ let decl = (Declare.ParameterEntry (None,(typ,univs),inl), IsAssumption kind) in
let kn = declare_constant ident ~local decl in
let gr = ConstRef kn in
let () = maybe_declare_manual_implicits false gr imps in
@@ -80,8 +80,8 @@ match scope with
let () = if do_instance then Classes.declare_instance env sigma None false gr in
let local = match local with ImportNeedQualified -> true | ImportDefaultBehavior -> false in
let () = if is_coe then Class.try_add_new_coercion gr ~local ~poly in
- let inst = match ctx with
- | Polymorphic_entry (_, ctx) -> Univ.UContext.instance ctx
+ let inst = match univs with
+ | Polymorphic_entry (_, univs) -> Univ.UContext.instance univs
| Monomorphic_entry _ -> Univ.Instance.empty
in
(gr,inst,Lib.is_modtype_strict ())
@@ -97,11 +97,11 @@ let next_uctx =
| Polymorphic_entry _ as uctx -> uctx
| Monomorphic_entry _ -> empty_uctx
-let declare_assumptions idl is_coe ~scope ~poly ~kind (c,uctx) pl imps nl =
+let declare_assumptions idl is_coe ~scope ~poly ~kind typ uctx pl imps nl =
let refs, status, _ =
List.fold_left (fun (refs,status,uctx) id ->
let ref',u',status' =
- declare_assumption is_coe ~scope ~poly ~kind (c,uctx) pl imps false nl id in
+ declare_assumption is_coe ~scope ~poly ~kind typ uctx pl imps false nl id in
(ref',u')::refs, status' && status, next_uctx uctx)
([],true,uctx) idl
in
@@ -178,9 +178,9 @@ let do_assumptions ~program_mode ~poly ~scope ~kind nl l =
let sigma = Evd.restrict_universe_context sigma uvars in
let uctx = Evd.check_univ_decl ~poly sigma udecl in
let ubinders = Evd.universe_binders sigma in
- pi2 (List.fold_left (fun (subst,status,uctx) ((is_coe,idl),t,imps) ->
- let t = replace_vars subst t in
- let refs, status' = declare_assumptions idl is_coe ~poly ~scope ~kind (t,uctx) ubinders imps nl in
+ pi2 (List.fold_left (fun (subst,status,uctx) ((is_coe,idl),typ,imps) ->
+ let typ = replace_vars subst typ in
+ let refs, status' = declare_assumptions idl is_coe ~poly ~scope ~kind typ uctx ubinders imps nl in
let subst' = List.map2
(fun {CAst.v=id} (c,u) -> (id, Constr.mkRef (c,u)))
idl refs
@@ -294,7 +294,7 @@ let context ~poly l =
if Lib.sections_are_opened () then DeclareDef.Discharge else DeclareDef.Global ImportDefaultBehavior in
let nstatus = match b with
| None ->
- pi3 (declare_assumption false ~scope ~poly ~kind:Context (t, univs) UnivNames.empty_binders [] impl
+ pi3 (declare_assumption false ~scope ~poly ~kind:Context t univs UnivNames.empty_binders [] impl
Declaremods.NoInline (CAst.make id))
| Some b ->
let entry = Declare.definition_entry ~univs ~types:t b in
diff --git a/vernac/comAssumption.mli b/vernac/comAssumption.mli
index 0a4130ee13..57b4aea9e3 100644
--- a/vernac/comAssumption.mli
+++ b/vernac/comAssumption.mli
@@ -31,7 +31,8 @@ val declare_assumption
-> poly:bool
-> scope:DeclareDef.locality
-> kind:assumption_object_kind
- -> Constr.types Entries.in_universes_entry
+ -> Constr.types
+ -> Entries.universes_entry
-> UnivNames.universe_binders
-> Impargs.manual_implicits
-> bool (** implicit *)
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 380ccff996..173a83f1d1 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -266,7 +266,7 @@ let save_remaining_recthms env sigma ~poly ~scope norm univs body opaq i
Univ.ContextSet.of_context univs
| Monomorphic_entry univs -> univs
in
- let c = SectionLocalAssum ((t_i, univs),poly,impl) in
+ let c = SectionLocalAssum {typ=t_i;univs;poly;impl} in
let _ = declare_variable name (Lib.cwd(),c,k) in
(VarRef name,impargs)
| Global local ->
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 13:03:05 +0000