From 97b58235341da0cfa3fdd88b0436f6d19be0a400 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Tue, 12 Feb 2002 10:42:32 +0000
Subject: suppression de la condition de la permutation case/fun

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

diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml
index 26c88726e7..9cbbf15f61 100644
--- a/contrib/extraction/mlutil.ml
+++ b/contrib/extraction/mlutil.ml
@@ -407,12 +407,11 @@ and simpl_case o br e =
 	try (* Is each branch independant of [e] ? *) 
 	  check_constant_case br 
 	with Impossible ->
-	  if (is_atomic e) then (* Swap the case and the lam if possible *)
-	    let ids,br = permut_case_fun br [] in 
-	    let n = List.length ids in 
-	    if n = 0 then MLcase (e, br) 
-	    else named_lams (MLcase (ml_lift n e, br)) ids
-	  else MLcase (e, br)
+	  (* Swap the case and the lam if possible *)
+	  let ids,br = permut_case_fun br [] in 
+	  let n = List.length ids in 
+	  if n = 0 then MLcase (e, br) 
+	  else named_lams (MLcase (ml_lift n e, br)) ids
 
 (*s Local [prop] elimination. *) 
 (* Try to eliminate as many [prop] as possible inside an [ml_ast]. *)
-- 
cgit v1.2.3