diff options
| author | herbelin | 2009-10-03 10:11:35 +0000 |
|---|---|---|
| committer | herbelin | 2009-10-03 10:11:35 +0000 |
| commit | 32222d67e21922966a49dccff81f99dd7ef5ec05 (patch) | |
| tree | b028dbd36847f111a0d535c00c44b6bf2dff3960 /kernel | |
| parent | feb92894c6be249abadd3303cfca3b258d6f3ea8 (diff) | |
Added option "Unset Dependent Propositions Elimination" to protect
against the incompatibilities introduced by making "destruct" working
on dependent propositions (incompatibilities come from uses of
destruct in Ltac definitions such as "destruct_conjs").
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12367 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions