diff options
| author | Hugo Herbelin | 2014-06-30 09:24:00 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2014-06-30 17:23:10 +0200 |
| commit | a0ccd7bdc29c35dd291a526891fdbb9909b8e827 (patch) | |
| tree | df984988850c92ffe32d0e57edfa482f931675ee /kernel/nativelambda.mli | |
| parent | 1f0f842e92be66f67044bdc6deb70676f0ffc22f (diff) | |
Synchronized names from the "as" clause with the skeleton of the
elimination scheme in induction/destruct also for those names which
correspond to neither the induction hypotheses nor the recursive
arguments.
Diffstat (limited to 'kernel/nativelambda.mli')
0 files changed, 0 insertions, 0 deletions