diff options
| author | glondu | 2011-03-31 09:39:21 +0000 |
|---|---|---|
| committer | glondu | 2011-03-31 09:39:21 +0000 |
| commit | 6d10a4751154cfb8149398d37c8dbde775adbf1c (patch) | |
| tree | 2583c7cfff8b5bb681d4d43d232083f3e46c131e /plugins/xml/xmlcommand.mli | |
| parent | 02041d9c285cd18d14b6233b437e7bff073114ed (diff) | |
Extraction: customized inductives are always standard
If the user customized the inductive, he should know what he is
doing... This (hopefully) fixes bug #2482.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13944 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/xml/xmlcommand.mli')
0 files changed, 0 insertions, 0 deletions