From e2a81df304c198cc2bdd5d1ffa703ed7eaca9d12 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 23 Jul 2017 04:08:30 +0200
Subject: Remove a few useless evar-normalizations in printing code.

---
 vernac/himsg.ml         | 2 +-
 vernac/vernacentries.ml | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'vernac')

diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index 784c6d3387..0e51849058 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -783,7 +783,7 @@ let pr_constraints printenv env sigma evars cstrs =
 
 let explain_unsatisfiable_constraints env sigma constr comp =
   let (_, constraints) = Evd.extract_all_conv_pbs sigma in
-  let undef = Evd.undefined_map (Evarutil.nf_evar_map_undefined sigma) in
+  let undef = Evd.undefined_map sigma in
   (** Only keep evars that are subject to resolution and members of the given
      component. *)
   let is_kept evk evi = match comp with
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 9650ea19d7..ce035522ae 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -65,7 +65,7 @@ let show_top_evars () =
   let pfts = Proof_global.give_me_the_proof () in
   let gls = Proof.V82.subgoals pfts in
   let sigma = gls.Evd.sigma in
-  Feedback.msg_notice (pr_evars_int sigma 1 (Evarutil.non_instantiated sigma))
+  Feedback.msg_notice (pr_evars_int sigma 1 (Evd.undefined_map sigma))
 
 let show_universes () =
   let pfts = Proof_global.give_me_the_proof () in
-- 
cgit v1.2.3