diff options
| author | Maxime Dénès | 2017-08-01 13:02:18 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-08-01 13:02:18 +0200 |
| commit | a893cd2993acb8da5a17aa57694ded2355e8eaea (patch) | |
| tree | 00f98278bbac7b25924ef5b1a7d4220dd540f491 /vernac | |
| parent | ec0fcba55a6849fa37438809df4783e7c5aa3a89 (diff) | |
| parent | e2a81df304c198cc2bdd5d1ffa703ed7eaca9d12 (diff) | |
Merge PR #919: 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 959df89f6e..adf24d23b1 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 |