diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-12-18 23:56:06 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-12-18 23:56:06 +0000 |
| commit | dadfbd96378d4c1b794ffc341bd10cc4d63b225d (patch) | |
| tree | 7ff1c2d295f7ff831302b92de6f00f686d0c9f3b /toplevel | |
| parent | 5536b6d56226c4e53bbd6c5ae9a2c419c6f08874 (diff) | |
Granted legitimate wish #2607 (not exposing crude fixpoint body of
unfolded fixpoints when calling destruct). However, this might break
compatibility.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14823 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel')
0 files changed, 0 insertions, 0 deletions