diff options
| author | Maxime Dénès | 2017-08-29 14:34:17 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-08-29 14:34:17 +0200 |
| commit | 75d70664156bf1715b4eb9933a684a344f43467d (patch) | |
| tree | 0f98f6fb7b1d39e8aae86c45ba7b2e36b3a91f53 /interp/declare.mli | |
| parent | 0c566066f92728d9a848e1f60f52dd09c1a727f2 (diff) | |
| parent | 2def58217686b5083da38778a5ebffb451b1d4d6 (diff) | |
Merge PR #773: [flags] Remove XML output flag.
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 6a09434645..ccd7d28bb5 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 |