From ff290c75151a8ba512a2a9e7dd9d4e37e23fe8dd Mon Sep 17 00:00:00 2001
From: letouzey
Date: Fri, 13 Dec 2002 13:51:35 +0000
Subject: une branche de case inutile

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

diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml
index 415921524e..4786215448 100644
--- a/contrib/extraction/extraction.ml
+++ b/contrib/extraction/extraction.ml
@@ -675,15 +675,13 @@ let extract_constant kn r =
 	       (* The real type [t']: without head lambdas, expanded, *)
 	       (* and with [Tvar] translated to [Tvar'] (not instantiable). *)
 	       let l,t' = type_decomp (type_expand (var2var' t)) in 
+	       let s = List.map ((<>) Tdummy) l in 
 	       (* The initial ML environment. *)
 	       let mle = List.fold_left Mlenv.push_std_type Mlenv.empty l in 
 	       (* The real extraction: *)
 	       let e = extract_term env mle t' c [] in
-	       if e = MLdummy then Dterm (r, MLdummy, Tdummy)
-	       else 
-		 (* Expunging term and type from dummy lambdas. *) 
-		 let s = List.map ((<>) Tdummy) l in 
-		 Dterm (r, term_expunge s (ids,e), type_expunge t)
+	       (* Expunging term and type from dummy lambdas. *) 
+	       Dterm (r, term_expunge s (ids,e), type_expunge t)
 	   | (Info, TypeScheme) -> 
 	       let body = Declarations.force l_body in
 	       let s,vl = type_sign_vl env typ in 
-- 
cgit v1.2.3