From 6b691bbd2101fd39395c0d2135fd7c06a8915e14 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Fri, 24 Dec 2010 11:53:29 +0100
Subject: Imported Upstream version 8.3pl1

---
 plugins/extraction/extraction.ml | 24 ++++++++++++++++--------
 1 file changed, 16 insertions(+), 8 deletions(-)

(limited to 'plugins/extraction/extraction.ml')

diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index b615955f..5329c675 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 13427 2010-09-17 17:37:52Z letouzey $ i*)
+(*i $Id: extraction.ml 13733 2010-12-21 13:08:53Z letouzey $ i*)
 
 (*i*)
 open Util
@@ -29,7 +29,7 @@ open Table
 open Mlutil
 (*i*)
 
-exception I of inductive_info
+exception I of inductive_kind
 
 (* A set of all fixpoint functions currently being extracted *)
 let current_fixpoints = ref ([] : constant list)
@@ -368,7 +368,7 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
     in
 
     add_ind kn mib
-      {ind_info = Standard;
+      {ind_kind = Standard;
        ind_nparams = npar;
        ind_packets = packets;
        ind_equiv = equiv
@@ -453,7 +453,7 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
 	Record field_glob
       with (I info) -> info
     in
-    let i = {ind_info = ind_info;
+    let i = {ind_kind = ind_info;
 	     ind_nparams = npar;
 	     ind_packets = packets;
 	     ind_equiv = equiv }
@@ -711,9 +711,15 @@ and extract_cons_app env mle mlt (((kn,i) as ip,j) as cp) args =
   let magic1 = needs_magic (type_cons, type_recomp (metas, a)) in
   let magic2 = needs_magic (a, mlt) in
   let head mla =
-    if mi.ind_info = Singleton then
+    if mi.ind_kind = Singleton then
       put_magic_if magic1 (List.hd mla) (* assert (List.length mla = 1) *)
-    else put_magic_if magic1 (MLcons (mi.ind_info, ConstructRef cp, mla))
+    else
+      let typeargs = match snd (type_decomp type_cons) with
+	| Tglob (_,l) -> List.map type_simpl l
+	| _ -> assert false
+      in
+      let info = {c_kind = mi.ind_kind; c_typs = typeargs} in
+      put_magic_if magic1 (MLcons (info, ConstructRef cp, mla))
   in
   (* Different situations depending of the number of arguments: *)
   if la < params_nb then
@@ -779,7 +785,7 @@ and extract_case env mle ((kn,i) as ip,c,br) mlt =
 	let e' = handle_exn r (List.length s) (fun _ -> Anonymous) e in
 	(r, List.rev ids, e')
       in
-      if mi.ind_info = Singleton then
+      if mi.ind_kind = Singleton then
 	begin
 	  (* Informative singleton case: *)
 	  (* [match c with C i -> t] becomes [let i = c' in t'] *)
@@ -790,7 +796,9 @@ and extract_case env mle ((kn,i) as ip,c,br) mlt =
 	end
       else
 	(* Standard case: we apply [extract_branch]. *)
-	MLcase ((mi.ind_info,BranchNone), a, Array.init br_size extract_branch)
+	let typs = List.map type_simpl (Array.to_list metas) in
+	let info = { m_kind = mi.ind_kind; m_typs = typs; m_same = BranchNone }
+	in MLcase (info, a, Array.init br_size extract_branch)
 
 (*s Extraction of a (co)-fixpoint. *)
 
-- 
cgit v1.2.3