diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-06-12 22:12:02 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-08-01 18:42:44 +0200 |
| commit | 2def58217686b5083da38778a5ebffb451b1d4d6 (patch) | |
| tree | c0c2463a4620fe3c6bb2caf21a70f6861bbb4643 /library/lib.mli | |
| parent | 65bd1deac80689d02be7ef580872974cc38bf93c (diff) | |
[flags] Remove XML output flag.
This is a second try at removing the hooks for the legacy xml export
system which can't currently be tested.
It is also not included in the API, so it should either be included in
it or this PR be applied.
Diffstat (limited to 'library/lib.mli')
| -rw-r--r-- | library/lib.mli | 6 |
1 files changed, 1 insertions, 5 deletions
diff --git a/library/lib.mli b/library/lib.mli index f1c9bfca2..3dcec1d53 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -150,10 +150,6 @@ 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 = Context.Named.Declaration.t * Decl_kinds.binding_kind type variable_context = variable_info list @@ -165,7 +161,7 @@ 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 val variable_section_segment_of_reference : Globnames.global_reference -> variable_context - + val section_instance : Globnames.global_reference -> Univ.universe_instance * Names.Id.t array val is_in_section : Globnames.global_reference -> bool |