diff options
| author | Hugo Herbelin | 2015-07-31 18:33:06 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2015-08-02 19:13:50 +0200 |
| commit | fdab811e58094accc02875c1f83e6476f4598d26 (patch) | |
| tree | 7951c6157dc4f0f8ed25063d2897577b0e5f46d8 /kernel | |
| parent | 817308ab59daa40bef09838cfc3d810863de0e46 (diff) | |
Removing the generalization of the body of inductive schemes from
Auto_ind_decl over the internal lemmas. The schemes are built in the
main process and the internal lemmas are actually already also in the
environment.
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions