diff options
Diffstat (limited to 'interp/declare.ml')
| -rw-r--r-- | interp/declare.ml | 15 |
1 files changed, 1 insertions, 14 deletions
diff --git a/interp/declare.ml b/interp/declare.ml index 70f422b51..7fcb38296 100644 --- a/interp/declare.ml +++ b/interp/declare.ml @@ -32,14 +32,6 @@ type internal_flag = | InternalTacticRequest (* kernel action, no message is displayed *) | UserIndividualRequest (* user action, a message is displayed *) -(** XML output hooks *) - -let (f_xml_declare_variable, xml_declare_variable) = Hook.make ~default:ignore () -let (f_xml_declare_constant, xml_declare_constant) = Hook.make ~default:ignore () -let (f_xml_declare_inductive, xml_declare_inductive) = Hook.make ~default:ignore () - -let if_xml f x = if !Flags.xml_export then f x else () - (** Declaration of section variables and local definitions *) type section_variable_entry = @@ -95,7 +87,6 @@ let declare_variable id obj = declare_var_implicits id; Notation.declare_ref_arguments_scope (VarRef id); Heads.declare_head (EvalVarRef id); - if_xml (Hook.get f_xml_declare_variable) oname; oname @@ -256,7 +247,6 @@ let declare_constant ?(internal = UserIndividualRequest) ?(local = false) id ?(e let id = Label.to_id (pi3 (Constant.repr3 c)) in ignore(add_leaf id o); update_tables c; - let () = if_xml (Hook.get f_xml_declare_constant) (InternalTacticRequest, c) in match role with | Safe_typing.Subproof -> () | Safe_typing.Schema (ind, kind) -> !declare_scheme kind [|ind,c|] @@ -268,9 +258,7 @@ let declare_constant ?(internal = UserIndividualRequest) ?(local = false) id ?(e cst_kind = kind; cst_locl = local; } in - let kn = declare_constant_common id cst in - let () = if_xml (Hook.get f_xml_declare_constant) (internal, kn) in - kn + declare_constant_common id cst let declare_definition ?(internal=UserIndividualRequest) ?(opaque=false) ?(kind=Decl_kinds.Definition) ?(local = false) @@ -410,7 +398,6 @@ let declare_mind mie = let isrecord,isprim = declare_projections mind in declare_mib_implicits mind; declare_inductive_argument_scopes mind mie; - if_xml (Hook.get f_xml_declare_inductive) (isrecord,oname); oname, isprim (* Declaration messages *) |