bug typage du cases/identity: optim off si inductif avec vars

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4234 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 10 insertions, 0 deletions

diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml
index 17e32a043..2805cd935 100644
--- a/contrib/extraction/mlutil.ml
+++ b/contrib/extraction/mlutil.ml
@@ -603,7 +603,17 @@ let check_and_generalize (r0,l,c) =
   same function [f] applied to the term matched. It is a generalized version 
   of the identity case optimization. *)
 
+(* CAVEAT: this optimization breaks typing in some special case. example: 
+   [type 'x a = A]. Then [let f = function A -> A] has type ['x a -> 'y a],
+   which is incompatible with the type of [let f x = x].
+   We brutally disable this optim for all inductive types with variables. *)
+
+
 let check_generalizable_case br = 
+  (match br.(0) with 
+     | ConstructRef ((kn,i),_), _, _ ->
+	 if (lookup_ind kn).ind_packets.(i).ip_vars <> [] then raise Impossible
+     | _ -> assert false); 
   let f = check_and_generalize br.(0) in 
   for i = 1 to Array.length br - 1 do 
     if check_and_generalize br.(i) <> f then raise Impossible