diff options
| author | Hugo Herbelin | 2020-10-04 21:51:35 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-10-06 21:59:07 +0200 |
| commit | 6acd4e8f15d11d4ed735092428398a3a27590f03 (patch) | |
| tree | b53f39a145f9ed2f6a3b373c0e9aa093056ed716 /pretyping/typeclasses_errors.mli | |
| parent | 3b8252d8990e715e5954812dffd0a5986cbb6012 (diff) | |
Fixing redundant outputs when printing goals, especially in non-"pr_first" mode.
Here is an example (see test output/goal_output.v for other examples):
2 subgoals, subgoal 1 (?Goal)
subgoal 1 (?Goal) is:
True
subgoal 2 (?Goal0) is:
True
This is now:
2 subgoals
subgoal 1 (?Goal) is:
True
subgoal 2 (?Goal0) is:
True
Diffstat (limited to 'pretyping/typeclasses_errors.mli')
0 files changed, 0 insertions, 0 deletions