diff options
| author |  glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-03-31 09:39:21 +0000 |
|---|---|---|
| committer | glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-03-31 09:39:21 +0000 |
| commit | 6d10a4751154cfb8149398d37c8dbde775adbf1c (patch) | |
| tree | 2583c7cfff8b5bb681d4d43d232083f3e46c131e | |
| 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
| -rw-r--r-- | plugins/extraction/extraction.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 450aa8710..51d79e821 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -382,6 +382,9 @@ and extract_ind env kn = (* kn is supposed to be in long form *) (* Third pass: we determine special cases. *) let ind_info = try + let ip = (kn, 0) in + let r = IndRef ip in + if is_custom r then raise (I Standard); if not mib.mind_finite then raise (I Coinductive); if mib.mind_ntypes <> 1 then raise (I Standard); let p = packets.(0) in @@ -393,9 +396,6 @@ and extract_ind env kn = (* kn is supposed to be in long form *) then raise (I Singleton); if l = [] then raise (I Standard); if not mib.mind_record then raise (I Standard); - let ip = (kn, 0) in - let r = IndRef ip in - if is_custom r then raise (I Standard); (* Now we're sure it's a record. *) (* First, we find its field names. *) let rec names_prod t = match kind_of_term t with |