From e3696e15775c44990018d1d4aea01c9bf662cd73 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Tue, 21 Dec 2010 11:31:57 +0000
Subject: Extraction: avoid type-unsafe optimisation of pattern-matchings (fix
 #2413)

 We now keep some type information in the "info" field of constructors
 and cases, and compact a match with some default branches (or remove
 this match completely) only if this transformation is type-preserving.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13732 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 plugins/extraction/modutil.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

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

diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml
index bb880aeea1..bff28aef15 100644
--- a/plugins/extraction/modutil.ml
+++ b/plugins/extraction/modutil.ml
@@ -80,10 +80,10 @@ let ast_iter_references do_term do_cons do_type a =
     match a with
       | MLglob r -> do_term r
       | MLcons (i,r,_) ->
-	  if lang () = Ocaml then record_iter_references do_term i;
+	  if lang () = Ocaml then record_iter_references do_term i.c_kind;
 	  do_cons r
       | MLcase (i,_,v) ->
-	  if lang () = Ocaml then record_iter_references do_term (fst i);
+	  if lang () = Ocaml then record_iter_references do_term i.m_kind;
 	  Array.iter (fun (r,_,_) -> do_cons r) v
       | _ -> ()
   in iter a
@@ -99,7 +99,7 @@ let ind_iter_references do_term do_cons do_type kn ind =
 	 | _ -> ());
     Array.iteri (fun j -> cons_iter (ip,j+1)) p.ip_types
   in
-  if lang () = Ocaml then record_iter_references do_term ind.ind_info;
+  if lang () = Ocaml then record_iter_references do_term ind.ind_kind;
     Array.iteri (fun i -> packet_iter (kn,i)) ind.ind_packets
 
 let decl_iter_references do_term do_cons do_type =
-- 
cgit v1.2.3