diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/decls.ml | 3 | ||||
| -rw-r--r-- | library/global.mli | 4 | ||||
| -rw-r--r-- | library/lib.mli | 8 |
3 files changed, 7 insertions, 8 deletions
diff --git a/library/decls.ml b/library/decls.ml index 8d5085f70..b5f9143b8 100644 --- a/library/decls.ml +++ b/library/decls.ml @@ -11,7 +11,6 @@ open Util open Names -open Context open Decl_kinds open Libnames @@ -55,7 +54,7 @@ let initialize_named_context_for_proof () = Environ.push_named_context_val d signv) sign Environ.empty_named_context_val let last_section_hyps dir = - fold_named_context + Context.Named.fold_outside (fun (id,_,_) sec_ids -> try if DirPath.equal dir (variable_path id) then id::sec_ids else sec_ids with Not_found -> sec_ids) diff --git a/library/global.mli b/library/global.mli index 09ed4eb0a..d6547105d 100644 --- a/library/global.mli +++ b/library/global.mli @@ -21,7 +21,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_context +val named_context : unit -> Context.Named.t (** {6 Enriching the global environment } *) @@ -73,7 +73,7 @@ val add_module_parameter : (** {6 Queries in the global environment } *) -val lookup_named : variable -> Context.named_declaration +val lookup_named : variable -> Context.Named.Declaration.t val lookup_constant : constant -> Declarations.constant_body val lookup_inductive : inductive -> Declarations.mutual_inductive_body * Declarations.one_inductive_body diff --git a/library/lib.mli b/library/lib.mli index bb8831759..874fc89fb 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -164,7 +164,7 @@ type variable_context = variable_info list type abstr_info = variable_context * Univ.universe_level_subst * Univ.UContext.t val instance_from_variable_context : variable_context -> Names.Id.t array -val named_of_variable_context : variable_context -> Context.named_context +val named_of_variable_context : variable_context -> Context.Named.t val section_segment_of_constant : Names.constant -> abstr_info val section_segment_of_mutual_inductive: Names.mutual_inductive -> abstr_info @@ -175,8 +175,8 @@ val is_in_section : Globnames.global_reference -> bool val add_section_variable : Names.Id.t -> Decl_kinds.binding_kind -> Decl_kinds.polymorphic -> Univ.universe_context_set -> unit val add_section_context : Univ.universe_context_set -> unit val add_section_constant : bool (* is_projection *) -> - Names.constant -> Context.named_context -> unit -val add_section_kn : Names.mutual_inductive -> Context.named_context -> unit + Names.constant -> Context.Named.t -> unit +val add_section_kn : Names.mutual_inductive -> Context.Named.t -> unit val replacement_context : unit -> Opaqueproof.work_list (** {6 Discharge: decrease the section level if in the current section } *) @@ -189,6 +189,6 @@ val discharge_inductive : Names.inductive -> Names.inductive (* discharging a constant in one go *) val full_replacement_context : unit -> Opaqueproof.work_list list val full_section_segment_of_constant : - Names.constant -> (Context.named_context -> Context.named_context) list + Names.constant -> (Context.Named.t -> Context.Named.t) list |