diff options
| author | Hugo Herbelin | 2014-11-09 14:39:58 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2014-11-22 19:23:32 +0100 |
| commit | 7610784dfed98b2510376217ab9ff1a444c6a2b4 (patch) | |
| tree | 5064708863270ddd0769196e89a610cbb84dbe3a /dev/base_include | |
| parent | 2224819115ef9eb655e516a590f046bf1c30a6ea (diff) | |
Not using an (arbitrary) pivot anymore for re-introduction of
quantified hypothesis in functional induction. This has apparently no
visible effect, probably because functional schemes do not have
non-dependent hypothesis in their branches besides induction
hypotheses which are anyway introduced at the top of the context.
Diffstat (limited to 'dev/base_include')
0 files changed, 0 insertions, 0 deletions