diff options
author | Stephane Glondu <steph@glondu.net> | 2011-04-19 16:44:20 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2011-04-19 16:44:20 +0200 |
commit | 9d27ae09786866b6e3d7b79d1fa7667e5e2aa309 (patch) | |
tree | a418d1edb3d53cdb4185b9719b7a70822cf5a24d /plugins/extraction/extraction.ml | |
parent | 6b691bbd2101fd39395c0d2135fd7c06a8915e14 (diff) |
Imported Upstream version 8.3.pl2upstream/8.3.pl2
Diffstat (limited to 'plugins/extraction/extraction.ml')
-rw-r--r-- | plugins/extraction/extraction.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 5329c675..b9a3a736 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: extraction.ml 13733 2010-12-21 13:08:53Z letouzey $ i*) +(*i $Id: extraction.ml 13795 2011-01-22 14:43:06Z glondu $ i*) (*i*) open Util @@ -394,6 +394,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 @@ -405,9 +408,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 |