diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/global.mli | 4 | ||||
| -rw-r--r-- | library/lib.ml | 2 | ||||
| -rw-r--r-- | library/lib.mli | 9 |
3 files changed, 8 insertions, 7 deletions
diff --git a/library/global.mli b/library/global.mli index 57e173cb9..b2a191cee 100644 --- a/library/global.mli +++ b/library/global.mli @@ -23,7 +23,7 @@ val env_is_initial : unit -> bool val universes : unit -> UGraph.t val named_context_val : unit -> Environ.named_context_val -val named_context : unit -> Context.Named.t +val named_context : unit -> Constr.named_context (** {6 Enriching the global environment } *) @@ -79,7 +79,7 @@ val add_module_parameter : (** {6 Queries in the global environment } *) -val lookup_named : variable -> Context.Named.Declaration.t +val lookup_named : variable -> Constr.named_declaration val lookup_constant : Constant.t -> Declarations.constant_body val lookup_inductive : inductive -> Declarations.mutual_inductive_body * Declarations.one_inductive_body diff --git a/library/lib.ml b/library/lib.ml index 128b27e75..a20de55bf 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -405,7 +405,7 @@ let find_opening_node id = - the list of substitution to do at section closing *) -type variable_info = Context.Named.Declaration.t * Decl_kinds.binding_kind +type variable_info = Constr.named_declaration * Decl_kinds.binding_kind type variable_context = variable_info list type abstr_info = { diff --git a/library/lib.mli b/library/lib.mli index 1d77212e9..5abfccfc7 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -9,6 +9,7 @@ (************************************************************************) open Names + (** Lib: record of operations, backtrack, low-level sections *) (** This module provides a general mechanism to keep a trace of all operations @@ -153,7 +154,7 @@ val unfreeze : frozen -> unit val init : unit -> unit (** {6 Section management for discharge } *) -type variable_info = Context.Named.Declaration.t * Decl_kinds.binding_kind +type variable_info = Constr.named_declaration * Decl_kinds.binding_kind type variable_context = variable_info list type abstr_info = private { abstr_ctx : variable_context; @@ -165,7 +166,7 @@ type abstr_info = private { } val instance_from_variable_context : variable_context -> Id.t array -val named_of_variable_context : variable_context -> Context.Named.t +val named_of_variable_context : variable_context -> Constr.named_context val section_segment_of_constant : Constant.t -> abstr_info val section_segment_of_mutual_inductive: MutInd.t -> abstr_info @@ -179,9 +180,9 @@ 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_context : Univ.ContextSet.t -> unit val add_section_constant : Decl_kinds.polymorphic -> - Constant.t -> Context.Named.t -> unit + Constant.t -> Constr.named_context -> unit val add_section_kn : Decl_kinds.polymorphic -> - MutInd.t -> Context.Named.t -> unit + MutInd.t -> Constr.named_context -> unit val replacement_context : unit -> Opaqueproof.work_list (** {6 Discharge: decrease the section level if in the current section } *) |