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 /interp/declare.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 'interp/declare.mli')
| -rw-r--r-- | interp/declare.mli | 5 |
1 files changed, 0 insertions, 5 deletions
diff --git a/interp/declare.mli b/interp/declare.mli index 6a0943464..ccd7d28bb 100644 --- a/interp/declare.mli +++ b/interp/declare.mli @@ -69,11 +69,6 @@ val set_declare_scheme : the whole block and a boolean indicating if it is a primitive record. *) val declare_mind : mutual_inductive_entry -> object_name * bool -(** Hooks for XML output *) -val xml_declare_variable : (object_name -> unit) Hook.t -val xml_declare_constant : (internal_flag * constant -> unit) Hook.t -val xml_declare_inductive : (bool * object_name -> unit) Hook.t - (** Declaration messages *) val definition_message : Id.t -> unit |