diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-08-01 13:02:18 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-08-01 13:02:18 +0200 |
| commit | a893cd2993acb8da5a17aa57694ded2355e8eaea (patch) | |
| tree | 00f98278bbac7b25924ef5b1a7d4220dd540f491 /printing/printer.ml | |
| parent | ec0fcba55a6849fa37438809df4783e7c5aa3a89 (diff) | |
| parent | e2a81df304c198cc2bdd5d1ffa703ed7eaca9d12 (diff) | |
Merge PR #919: Remove a few useless evar-normalizations in printing code.
Diffstat (limited to 'printing/printer.ml')
| -rw-r--r-- | printing/printer.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/printing/printer.ml b/printing/printer.ml index f731a39a4..c6cf2254f 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -727,7 +727,7 @@ let default_pr_subgoals ?(pr_first=true) match goals with | [] -> begin - let exl = Evarutil.non_instantiated sigma in + let exl = Evd.undefined_map sigma in if Evar.Map.is_empty exl then (str"No more subgoals." ++ print_dependent_evars None sigma seeds) else |