diff options
| author | herbelin | 2009-09-27 07:56:55 +0000 |
|---|---|---|
| committer | herbelin | 2009-09-27 07:56:55 +0000 |
| commit | f99dc2691ace6a691e7fd07e580e855e7bca7b55 (patch) | |
| tree | 3ae1ac05155169ea776d573e7ee4ce5a42f592eb /plugins/pluginsopt.itarget | |
| parent | b7a2a4728aae75eba4750b7c3e0dc60c624b76cf (diff) | |
Delay the choice of eliminator in destruct/induction until we know if
a dependent scheme is needed or not (this allows for instance
"destruct H" when H is propositional and dependent in the context to
work).
Modest attempt to clarify the basic components used and invariants
preserved when sharing the code for functional induction and for
destruct/induction.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12356 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/pluginsopt.itarget')
0 files changed, 0 insertions, 0 deletions