diff options
| author | Pierre-Marie Pédrot | 2017-07-23 04:08:30 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-07-26 15:42:46 +0200 |
| commit | e2a81df304c198cc2bdd5d1ffa703ed7eaca9d12 (patch) | |
| tree | e38618f0a419d539bb1375334a56fc928a468591 /vernac | |
| parent | bd1a0abf49fe67e7f02dc562d4b81d27ed6f606c (diff) | |
Remove a few useless evar-normalizations in printing code.
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 |