diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2014-08-04 17:50:36 -0400 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2014-08-04 18:10:12 -0400 |
| commit | 87a60c55292e6e9f8dbcfec4d64cb9ae940618f9 (patch) | |
| tree | 4b4fc014e7d6cf28c42a63016522eb5be56e1afb /plugins/setoid_ring/Ring_polynom.v | |
| parent | f128088974e9ba543ca51ab76a92ff085def9728 (diff) | |
One more optimization for guard checking of cofixpoints.
In check_one_cofix, we now avoid calling dest_subterms each time we meet a
constructor by storing both the current tree (needed for the new criterion)
and a precomputed array of trees for subterms.
Diffstat (limited to 'plugins/setoid_ring/Ring_polynom.v')
0 files changed, 0 insertions, 0 deletions