diff options
| author | Pierre-Marie Pédrot | 2019-07-31 13:32:25 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-07-31 14:35:23 +0200 |
| commit | fc60feb7a3ccd9ec88f6c46929f5fa8172bd7885 (patch) | |
| tree | 309674e4e3debf44ca7c10b07e429f75022c9dd6 /library/lib.mli | |
| parent | 162eefb562aca2c3741ec24d201deb881663e05a (diff) | |
Specialize the section API.
We split the function used to retrieve the local context from the one used to
provide the implicit status of each binder. Most of the users only rely on the
former indeed.
Diffstat (limited to 'library/lib.mli')
| -rw-r--r-- | library/lib.mli | 7 |
1 files changed, 3 insertions, 4 deletions
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 |