4 files changed, 6 insertions, 8 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 33a86402ef..87b31849ee 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -433,7 +433,7 @@ let explain_no_such_bound_variable evd id =
     | Cltyp (na, _) -> na
     | Clval (na, _, _) -> na
     in
-    if na != Anonymous then out_name na :: l else l
+    if na != Anonymous then Name.get_id na :: l else l
   in
   let mvl = List.fold_left fold [] (Evd.meta_list evd) in
   user_err ~hdr:"Evd.meta_with_name"
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 259e96a276..91e6dc4ab2 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -188,8 +188,6 @@ let tclSHOWHYPS (tac : tactic) (goal: Goal.goal Evd.sigma)
       (fun hypl -> List.subtract cmp hypl oldhyps)
       hyps
   in
-  let emacs_str s =
-    if !Flags.print_emacs then s else "" in
   let s = 
     let frst = ref true in
     List.fold_left
@@ -199,9 +197,9 @@ let tclSHOWHYPS (tac : tactic) (goal: Goal.goal Evd.sigma)
 	   "" lh))
     "" newhyps in
   Feedback.msg_notice
-    (str (emacs_str "<infoH>")
+    (str "<infoH>"
       ++  (hov 0 (str s))
-      ++  (str (emacs_str "</infoH>")));
+      ++  (str "</infoH>"));
   tclIDTAC goal;;
 
 
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 97c5cda770..66d91c634a 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -75,7 +75,7 @@ let pf_get_new_ids ids gls =
     (fun id acc -> (next_ident_away id (acc@avoid))::acc)
     ids []
 
-let pf_global gls id = EConstr.of_constr (Constrintern.construct_reference (pf_hyps gls) id)
+let pf_global gls id = EConstr.of_constr (Universes.constr_of_global (Constrintern.construct_reference (pf_hyps gls) id))
 
 let pf_reduction_of_red_expr gls re c =
   let (redfun, _) = reduction_of_red_expr (pf_env gls) re in
@@ -171,7 +171,7 @@ module New = struct
     (** We only check for the existence of an [id] in [hyps] *)
     let gl = Proofview.Goal.assume gl in
     let hyps = Proofview.Goal.hyps gl in
-    EConstr.of_constr (Constrintern.construct_reference hyps id)
+    Constrintern.construct_reference hyps id
 
   let pf_env = Proofview.Goal.env
   let pf_concl = Proofview.Goal.concl
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index e6e60e27f7..1172e55ac6 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -100,7 +100,7 @@ val pr_glls   : goal list sigma -> Pp.std_ppcmds
 (* Variants of [Tacmach] functions built with the new proof engine *)
 module New : sig
   val pf_apply : (env -> evar_map -> 'a) -> ('b, 'r) Proofview.Goal.t -> 'a
-  val pf_global : identifier -> ('a, 'r) Proofview.Goal.t -> constr
+  val pf_global : identifier -> ('a, 'r) Proofview.Goal.t -> Globnames.global_reference
   (** FIXME: encapsulate the level in an existential type. *)
   val of_old : (Proof_type.goal Evd.sigma -> 'a) -> ([ `NF ], 'r) Proofview.Goal.t -> 'a