diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/lib.ml | 22 | ||||
| -rw-r--r-- | library/lib.mli | 7 |
2 files changed, 15 insertions, 14 deletions
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 |