aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/vernacentries.ml
diff options
context:
space:
mode:
Diffstat (limited to 'vernac/vernacentries.ml')
-rw-r--r--vernac/vernacentries.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 9650ea19d..ce035522a 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