diff options
| author | msozeau | 2012-02-20 20:54:12 +0000 |
|---|---|---|
| committer | msozeau | 2012-02-20 20:54:12 +0000 |
| commit | 7c4d29628a58d0192b76aebf8da29644019aee1c (patch) | |
| tree | 227905d3fe5e4f75a3f144c15fb8871725c74335 /kernel | |
| parent | 70621433c2c4028650e1c09e88c496f0aba67a6f (diff) | |
Use a heuristic to not simplify equality hypotheses remaining after dependent induction if they
don't look really trivial. We still are making a choice though. Fixes bug #2712.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14988 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions