summaryrefslogtreecommitdiff
path: root/contrib/extraction/extraction.ml
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2007-10-15 19:55:12 +0000
committerGravatar Samuel Mimram <smimram@debian.org>2007-10-15 19:55:12 +0000
commit4767d724d489a7ad67f696e9401e70b9f9ae2143 (patch)
tree142a99bc1cd3beef403f1942908de090f70c5e07 /contrib/extraction/extraction.ml
parent72b9a7df489ea47b3e5470741fd39f6100d31676 (diff)
Imported Upstream version 8.1.pl2+dfsgupstream/8.1.pl2+dfsg
Diffstat (limited to 'contrib/extraction/extraction.ml')
-rw-r--r--contrib/extraction/extraction.ml25
1 files changed, 11 insertions, 14 deletions
diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml
index 6fd4a3cc..6982ffc6 100644
--- a/contrib/extraction/extraction.ml
+++ b/contrib/extraction/extraction.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: extraction.ml 9456 2006-12-17 20:08:38Z letouzey $ i*)
+(*i $Id: extraction.ml 10195 2007-10-08 01:47:55Z letouzey $ i*)
(*i*)
open Util
@@ -31,10 +31,6 @@ open Mlutil
exception I of inductive_info
-(* A set of all inductive currently being computed,
- to avoid loops in [extract_inductive] *)
-let internal_call = ref KNset.empty
-
(* A set of all fixpoint functions currently being extracted *)
let current_fixpoints = ref ([] : constant list)
@@ -303,13 +299,15 @@ and extract_type_scheme env db c p =
(*S Extraction of an inductive type. *)
and extract_ind env kn = (* kn is supposed to be in long form *)
- try
- if KNset.mem kn !internal_call then lookup_ind kn (* Already started. *)
- else if visible_kn kn then lookup_ind kn (* Standard situation. *)
- else raise Not_found (* Never trust the table for a internal kn. *)
+ let mib = Environ.lookup_mind kn env in
+ try
+ (* For a same kn, we can get various bodies due to module substitutions.
+ We hence check that the mib has not changed from recording
+ time to retrieving time. Ideally we should also check the env. *)
+ let (mib0,ml_ind) = lookup_ind kn in
+ if not (mib = mib0) then raise Not_found;
+ ml_ind
with Not_found ->
- internal_call := KNset.add kn !internal_call;
- let mib = Environ.lookup_mind kn env in
(* First, if this inductive is aliased via a Module, *)
(* we process the original inductive. *)
option_iter (fun kn -> ignore (extract_ind env kn)) mib.mind_equiv;
@@ -335,7 +333,7 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
ip_types = t })
mib.mind_packets
in
- add_ind kn
+ add_ind kn mib
{ind_info = Standard;
ind_nparams = npar;
ind_packets = packets;
@@ -425,8 +423,7 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
ind_packets = packets;
ind_equiv = mib.mind_equiv}
in
- add_ind kn i;
- internal_call := KNset.remove kn !internal_call;
+ add_ind kn mib i;
i
(*s [extract_type_cons] extracts the type of an inductive