From 6d10a4751154cfb8149398d37c8dbde775adbf1c Mon Sep 17 00:00:00 2001 From: glondu Date: Thu, 31 Mar 2011 09:39:21 +0000 Subject: 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 --- plugins/extraction/extraction.ml | 6 +++--- 1 file 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 -- cgit v1.2.3