diff options
author | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-10-20 09:39:28 +0200 |
---|---|---|
committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-10-20 23:29:19 +0200 |
commit | f00f8482e1d21ef8b03044ed2162cb29d9e4537d (patch) | |
tree | b49c6d121189c442dd73fea08402ee00a269f0cf /kernel/constr.ml | |
parent | 6e0c5c81e9e81c2e5369427643b2ac51b9aa17e6 (diff) |
Fixing a bug in the presence of let-in in inductive arity.
Diffstat (limited to 'kernel/constr.ml')
0 files changed, 0 insertions, 0 deletions