From ed7af646f2e486b7e96812ba2335e644756b70fd Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Tue, 27 Oct 2015 13:55:45 -0400 Subject: Fix bugs 4389, 4390 and 4391 due to wrong handling of universe names structure. --- library/lib.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'library/lib.mli') diff --git a/library/lib.mli b/library/lib.mli index 9c4d26c5b2..b67b2b873f 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -172,7 +172,7 @@ val section_instance : Globnames.global_reference -> Univ.universe_instance * Na 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 -- cgit v1.2.3 From 0a1b046d37761fe47435d5041bb5031e3f7d6613 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 28 Oct 2015 10:03:17 +0100 Subject: lib_stack: API to reorder the libstack For discharging it is important that constants occur in the libstack in an order that respects the dependencies among them. This is impossible to achieve for private constants when they are exported globally without this (ugly IMO) api. --- library/lib.mli | 1 + 1 file changed, 1 insertion(+) (limited to 'library/lib.mli') diff --git a/library/lib.mli b/library/lib.mli index b67b2b873f..bb88317591 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -55,6 +55,7 @@ val segment_of_objects : val add_leaf : Names.Id.t -> Libobject.obj -> Libnames.object_name val add_anonymous_leaf : Libobject.obj -> unit +val pull_to_head : Libnames.object_name -> unit (** this operation adds all objects with the same name and calls [load_object] for each of them *) -- cgit v1.2.3 From 9d991d36c07efbb6428e277573bd43f6d56788fc Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Fri, 8 Jan 2016 10:00:21 +0100 Subject: CLEANUP: kernel/context.ml{,i} The structure of the Context module was refined in such a way that: - Types and functions related to rel-context declarations were put into the Context.Rel.Declaration module. - Types and functions related to rel-context were put into the Context.Rel module. - Types and functions related to named-context declarations were put into the Context.Named.Declaration module. - Types and functions related to named-context were put into the Context.Named module. - Types and functions related to named-list-context declarations were put into Context.NamedList.Declaration module. - Types and functions related to named-list-context were put into Context.NamedList module. Some missing comments were added to the *.mli file. The output of ocamldoc was checked whether it looks in a reasonable way. "TODO: cleanup" was removed The order in which are exported functions listed in the *.mli file was changed. (as in a mature modules, this order usually is not random) The order of exported functions in Context.{Rel,Named} modules is now consistent. (as there is no special reason why that order should be different) The order in which are functions defined in the *.ml file is the same as the order in which they are listed in the *.mli file. (as there is no special reason to define them in a different order) The name of the original fold_{rel,named}_context{,_reverse} functions was changed to better indicate what those functions do. (Now they are called Context.{Rel,Named}.fold_{inside,outside}) The original comments originally attached to the fold_{rel,named}_context{,_reverse} did not full make sense so they were updated. Thrown exceptions are now documented. Naming of formal parameters was made more consistent across different functions. Comments of similar functions in different modules are now consistent. Comments from *.mli files were copied to *.ml file. (We need that information in *.mli files because that is were ocamldoc needs it. It is nice to have it also in *.ml files because when we are using Merlin and jump to the definion of the function, we can see the comments also there and do not need to open a different file if we want to see it.) When we invoke ocamldoc, we instruct it to generate UTF-8 HTML instead of (default) ISO-8859-1. (UTF-8 characters are used in our ocamldoc markup) "open Context" was removed from all *.mli and *.ml files. (Originally, it was OK to do that. Now it is not.) An entry to dev/doc/changes.txt file was added that describes how the names of types and functions have changed. --- library/lib.mli | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'library/lib.mli') diff --git a/library/lib.mli b/library/lib.mli index bb88317591..874fc89fb4 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 -- cgit v1.2.3 From 74a5cfa8b2f1a881ebf010160421cf0775c2a084 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Fri, 15 Jan 2016 17:49:49 +0100 Subject: Hooks for a third-party XML plugin. Contributed by Claudio Sacerdoti Coen. --- library/lib.mli | 4 ++++ 1 file changed, 4 insertions(+) (limited to 'library/lib.mli') diff --git a/library/lib.mli b/library/lib.mli index bb88317591..398149a50f 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -157,6 +157,10 @@ val unfreeze : frozen -> unit val init : unit -> unit +(** XML output hooks *) +val xml_open_section : (Names.Id.t -> unit) Hook.t +val xml_close_section : (Names.Id.t -> unit) Hook.t + (** {6 Section management for discharge } *) type variable_info = Names.Id.t * Decl_kinds.binding_kind * Term.constr option * Term.types -- cgit v1.2.3 From 86f5c0cbfa64c5d0949365369529c5b607878ef8 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 20 Jan 2016 17:25:10 +0100 Subject: Update copyright headers. --- library/lib.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'library/lib.mli') diff --git a/library/lib.mli b/library/lib.mli index 398149a50f..29fc7cd24b 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* 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 *) -> +val add_section_constant : Decl_kinds.polymorphic -> Names.constant -> Context.named_context -> unit -val add_section_kn : Names.mutual_inductive -> Context.named_context -> unit +val add_section_kn : Decl_kinds.polymorphic -> + Names.mutual_inductive -> Context.named_context -> unit val replacement_context : unit -> Opaqueproof.work_list (** {6 Discharge: decrease the section level if in the current section } *) -- cgit v1.2.3