4 files changed, 3 insertions, 24 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index fcaee5c939..54861ae4cc 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -1098,7 +1098,6 @@ let extern_constr_gen lax goal_concl_style scopt env sigma t =
   (* Not "goal_concl_style" means do alpha-conversion avoiding only *)
   (* those goal/section/rel variables that occurs in the subterm under *)
   (* consideration; see namegen.ml for further details *)
-  let t = EConstr.of_constr t in
   let avoid = if goal_concl_style then ids_of_context env else [] in
   let r = Detyping.detype ~lax:lax goal_concl_style avoid env sigma t in
   let vars = vars_of_env env in
@@ -1111,7 +1110,6 @@ let extern_constr ?(lax=false) goal_concl_style env sigma t =
   extern_constr_gen lax goal_concl_style None env sigma t
 
 let extern_type goal_concl_style env sigma t =
-  let t = EConstr.of_constr t in
   let avoid = if goal_concl_style then ids_of_context env else [] in
   let r = Detyping.detype goal_concl_style avoid env sigma t in
   extern_glob_type (vars_of_env env) r
@@ -1198,8 +1196,6 @@ let extern_constr_pattern env sigma pat =
   extern true (None,[]) Id.Set.empty (glob_of_pat env sigma pat)
 
 let extern_rel_context where env sigma sign =
-  let sign = List.map (fun d -> Termops.map_rel_decl EConstr.of_constr d) sign in
-  let where = Option.map EConstr.of_constr where in
   let a = detype_rel_context where [] (names_of_rel_context env,env) sigma sign in
   let vars = vars_of_env env in
   let a = List.map (extended_glob_local_binder_of_decl) a in
diff --git a/interp/constrextern.mli b/interp/constrextern.mli
index b5242b3477..ffa891c502 100644
--- a/interp/constrextern.mli
+++ b/interp/constrextern.mli
@@ -9,6 +9,7 @@
 open Names
 open Term
 open Termops
+open EConstr
 open Environ
 open Libnames
 open Globnames
@@ -41,7 +42,7 @@ val extern_reference : ?loc:Loc.t -> Id.Set.t -> global_reference -> reference
 val extern_type : bool -> env -> Evd.evar_map -> types -> constr_expr
 val extern_sort : Evd.evar_map -> sorts -> glob_sort
 val extern_rel_context : constr option -> env -> Evd.evar_map ->
-  Context.Rel.t -> local_binder_expr list
+  rel_context -> local_binder_expr list
 
 (** Printing options *)
 val print_implicits : bool ref
diff --git a/interp/declare.ml b/interp/declare.ml
index 70f422b514..7fcb38296f 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 *)
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