From 432e9f19e669c23c2ffd06a81a89e4318706991d Mon Sep 17 00:00:00 2001 From: letouzey Date: Thu, 10 Jul 2003 21:21:53 +0000 Subject: 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 --- contrib/extraction/mlutil.ml | 10 ++++++++++ 1 file changed, 10 insertions(+) (limited to 'contrib/extraction') 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 -- cgit v1.2.3