From 2def58217686b5083da38778a5ebffb451b1d4d6 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 12 Jun 2017 22:12:02 +0200 Subject: [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. --- library/lib.mli | 6 +----- 1 file changed, 1 insertion(+), 5 deletions(-) (limited to 'library/lib.mli') 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 -- cgit v1.2.3