diff options
| author |  Arnaud Spiwack <arnaud@spiwack.net> | 2015-02-19 12:08:51 +0100 |
|---|---|---|
| committer | Arnaud Spiwack <arnaud@spiwack.net> | 2015-02-24 18:50:39 +0100 |
| commit | f7b29094fe7cc13ea475447bd30d9a8b942f0fef (patch) | |
| tree | b1533a863e91a2650e2706b4955337f526249b36 /plugins/cc | |
| parent | fc6d0fb650f57a764af6fe9be44677a69be11980 (diff) | |
[Proofview.tclPROGRESS]: do not consider that trivial goal instantiation is progress.
Also compare goals up to evar instantiation (otherwise no progress would be observed when only unification occurs, unless some [nf_evar] is done). Performance look unchanged so far.
Some code from [Evd] which was used only in [tclPROGRESS] have been moved out (and [progress_evar_map] was now dead, so I killed it).
Fixes bugs (one reported directly on coqdev, and #3412).
Diffstat (limited to 'plugins/cc')
0 files changed, 0 insertions, 0 deletions