diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-10-28 03:13:26 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-03-29 02:44:27 +0200 |
| commit | d788f81df74f7ed2dd62488736f67f1ee596aee2 (patch) | |
| tree | a2567be7e94e2ffa6485a23efdf758e41c797713 /printing | |
| parent | bd8606189268c3fcdd3506872d459cb9032a33bf (diff) | |
Preparing old-style refine from logic.ml to deal with "Cases" proof
terms whose branches are in eta-let-expanded canonical form.
This is a hack intended to work only with destruct/case as they are
currently implemented. Would not work with arbitrary proofs of the
form "Cases(ci,p,c,[|...;b;...|] given to logic.ml for which b, if
with Metas, has not the form of an eta-let-expanded Meta.
Diffstat (limited to 'printing')
0 files changed, 0 insertions, 0 deletions