aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--interp/impargs.ml10
-rw-r--r--interp/notation.ml2
-rw-r--r--library/lib.ml22
-rw-r--r--library/lib.mli7
-rw-r--r--pretyping/arguments_renaming.ml2
-rw-r--r--tactics/declare.ml3
-rw-r--r--vernac/classes.ml2
7 files changed, 25 insertions, 23 deletions
diff --git a/interp/impargs.ml b/interp/impargs.ml
index 0466efa991..3f2a1b075c 100644
--- a/interp/impargs.ml
+++ b/interp/impargs.ml
@@ -487,11 +487,13 @@ let subst_implicits (subst,(req,l)) =
(ImplLocal,List.Smart.map (subst_implicits_decl subst) l)
let impls_of_context ctx =
- let map (decl, impl) = match impl with
- | Implicit -> Some (NamedDecl.get_id decl, Manual, (true, true))
- | _ -> None
+ let map decl =
+ let id = NamedDecl.get_id decl in
+ match Lib.variable_section_kind id with
+ | Implicit -> Some (id, Manual, (true, true))
+ | _ -> None
in
- List.rev_map map (List.filter (fst %> NamedDecl.is_local_assum) ctx)
+ List.rev_map map (List.filter (NamedDecl.is_local_assum) ctx)
let adjust_side_condition p = function
| LessArgsThan n -> LessArgsThan (n+p)
diff --git a/interp/notation.ml b/interp/notation.ml
index d88182241b..a78bc60e83 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -1533,7 +1533,7 @@ let discharge_arguments_scope (_,(req,r,n,l,_)) =
let n =
try
let vars = Lib.variable_section_segment_of_reference r in
- vars |> List.map fst |> List.filter is_local_assum |> List.length
+ vars |> List.filter is_local_assum |> List.length
with
Not_found (* Not a ref defined in this section *) -> 0 in
Some (req,r,n,l,[])
diff --git a/library/lib.ml b/library/lib.ml
index fa383ab23c..6b01eb07e9 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -413,11 +413,8 @@ let find_opening_node id =
- the list of substitution to do at section closing
*)
-type variable_info = Constr.named_declaration * Decl_kinds.binding_kind
-
-type variable_context = variable_info list
type abstr_info = {
- abstr_ctx : variable_context;
+ abstr_ctx : Constr.named_context;
abstr_subst : Univ.Instance.t;
abstr_uctx : Univ.AUContext.t;
}
@@ -426,7 +423,6 @@ type abstr_list = abstr_info Names.Cmap.t * abstr_info Names.Mindmap.t
type secentry =
| Variable of {
id:Names.Id.t;
- kind:Decl_kinds.binding_kind;
}
| Context of Univ.ContextSet.t
@@ -445,6 +441,9 @@ let empty_section_data ~poly = {
let sectab =
Summary.ref ([] : section_data list) ~name:"section-context"
+let sec_implicits =
+ Summary.ref Id.Map.empty ~name:"section-implicits"
+
let check_same_poly p sec =
if p != sec.sec_poly then
user_err Pp.(str "Cannot mix universe polymorphic and monomorphic declarations in sections.")
@@ -458,8 +457,9 @@ let add_section_variable ~name ~kind ~poly =
| [] -> () (* because (Co-)Fixpoint temporarily uses local vars *)
| s :: sl ->
List.iter (fun tab -> check_same_poly poly tab) !sectab;
- let s = { s with sec_entry = Variable {id=name;kind} :: s.sec_entry } in
- sectab := s :: sl
+ let s = { s with sec_entry = Variable {id=name} :: s.sec_entry } in
+ sectab := s :: sl;
+ sec_implicits := Id.Map.add name kind !sec_implicits
let add_section_context ctx =
match !sectab with
@@ -486,9 +486,9 @@ let is_polymorphic_univ u =
let extract_hyps poly (secs,ohyps) =
let rec aux = function
- | (Variable {id;kind}::idl, decl::hyps) when Names.Id.equal id (NamedDecl.get_id decl) ->
+ | (Variable {id}::idl, decl::hyps) when Names.Id.equal id (NamedDecl.get_id decl) ->
let l, r = aux (idl,hyps) in
- (decl,kind) :: l, r
+ decl :: l, r
| (Variable _::idl,hyps) ->
let l, r = aux (idl,hyps) in
l, r
@@ -500,7 +500,7 @@ let extract_hyps poly (secs,ohyps) =
in aux (secs,ohyps)
let instance_from_variable_context =
- List.rev_map fst %> List.filter is_local_assum %> List.map NamedDecl.get_id %> Array.of_list
+ List.rev %> List.filter is_local_assum %> List.map NamedDecl.get_id %> Array.of_list
let extract_worklist info =
let args = instance_from_variable_context info.abstr_ctx in
@@ -576,6 +576,8 @@ let section_segment_of_reference = let open GlobRef in function
let variable_section_segment_of_reference gr =
(section_segment_of_reference gr).abstr_ctx
+let variable_section_kind id = Id.Map.get id !sec_implicits
+
let section_instance = let open GlobRef in function
| VarRef id ->
let eq = function
diff --git a/library/lib.mli b/library/lib.mli
index bfee1b16c5..7dc8b52282 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -163,10 +163,8 @@ val drop_objects : frozen -> frozen
val init : unit -> unit
(** {6 Section management for discharge } *)
-type variable_info = Constr.named_declaration * Decl_kinds.binding_kind
-type variable_context = variable_info list
type abstr_info = private {
- abstr_ctx : variable_context;
+ abstr_ctx : Constr.named_context;
(** Section variables of this prefix *)
abstr_subst : Univ.Instance.t;
(** Actual names of the abstracted variables *)
@@ -178,7 +176,8 @@ val section_segment_of_constant : Constant.t -> abstr_info
val section_segment_of_mutual_inductive: MutInd.t -> abstr_info
val section_segment_of_reference : GlobRef.t -> abstr_info
-val variable_section_segment_of_reference : GlobRef.t -> variable_context
+val variable_section_segment_of_reference : GlobRef.t -> Constr.named_context
+val variable_section_kind : Id.t -> Decl_kinds.binding_kind
val section_instance : GlobRef.t -> Univ.Instance.t * Id.t array
val is_in_section : GlobRef.t -> bool
diff --git a/pretyping/arguments_renaming.ml b/pretyping/arguments_renaming.ml
index 534c0ca20b..a86d237164 100644
--- a/pretyping/arguments_renaming.ml
+++ b/pretyping/arguments_renaming.ml
@@ -47,7 +47,7 @@ let discharge_rename_args = function
| _, (ReqGlobal (c, names), _ as req) when not (isVarRef c && Lib.is_in_section c) ->
(try
let vars = Lib.variable_section_segment_of_reference c in
- let var_names = List.map (fst %> NamedDecl.get_id %> Name.mk_name) vars in
+ let var_names = List.map (NamedDecl.get_id %> Name.mk_name) vars in
let names' = var_names @ names in
Some (ReqGlobal (c, names), (c, names'))
with Not_found -> Some req)
diff --git a/tactics/declare.ml b/tactics/declare.ml
index 63e9279edc..61f9c3b1c5 100644
--- a/tactics/declare.ml
+++ b/tactics/declare.ml
@@ -71,8 +71,7 @@ let load_constant i ((sp,kn), obj) =
let cooking_info segment =
let modlist = replacement_context () in
- let { abstr_ctx = hyps; abstr_subst = subst; abstr_uctx = uctx } = segment in
- let named_ctx = List.map fst hyps in
+ let { abstr_ctx = named_ctx; abstr_subst = subst; abstr_uctx = uctx } = segment in
let abstract = (named_ctx, subst, uctx) in
{ Opaqueproof.modlist; abstract }
diff --git a/vernac/classes.ml b/vernac/classes.ml
index efe452d5f1..075d89d0df 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -179,7 +179,7 @@ let discharge_class (_,cl) =
let open CVars in
let repl = Lib.replacement_context () in
let rel_of_variable_context ctx = List.fold_right
- ( fun (decl,_) (ctx', subst) ->
+ ( fun decl (ctx', subst) ->
let decl' = decl |> NamedDecl.map_constr (substn_vars 1 subst) |> NamedDecl.to_rel_decl in
(decl' :: ctx', NamedDecl.get_id decl :: subst)
) ctx ([], []) in
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 13:38:57 +0000