diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-04-04 15:29:15 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-04-04 16:25:01 +0200 |
| commit | f65fa9de8a4c9c12d933188a755b51508bd51921 (patch) | |
| tree | b23aabea129cd2688be3c7ad8a483fc8ab4dcee1 /checker/closure.ml | |
| parent | 5b688868704cc1097aded2caea27d89047318eb1 (diff) | |
Fixing #3262 which revealed a non-progressing, hence looping,
refinement of evars (in filter_candidates).
Incidentally introduced a copy of type "option", "update", which
highlights the specific intention of "updating" or not.
Diffstat (limited to 'checker/closure.ml')
0 files changed, 0 insertions, 0 deletions