diff options
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/himsg.ml | 2 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 2 |
2 files changed, 2 insertions, 2 deletions
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 |