diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-06-01 17:38:33 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-06-01 17:38:33 +0000 |
| commit | 35e4ac349af4fabbc5658b5cba632f98ec04da3f (patch) | |
| tree | 4d93caa6c98f7a7b97e36c3523b2a3379ce89193 /pretyping/termops.ml | |
| parent | a9d9dd605645ab94336fef3976605e8394b816ce (diff) | |
Let's try to avoid generating induction principles for records (wish #2693)
Since record cannot be recursive, induction principles for them are
just wasted ressources. With this patch, we turn off there generation
by default. The flag "Set/Unset Record Elimination Schemes" allows
to start producing them again.
For compatibility, we adapt "induction" and similar tactics that
rely on the existence of induction principles : on a record,
"induction" is now silently converted into "destruct".
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15411 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/termops.ml')
0 files changed, 0 insertions, 0 deletions