From da33e695040678d74622213af2cd43d32140d186 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Mon, 12 Nov 2001 10:00:49 +0000
Subject: suite refonte extraction.ml

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

diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml
index 368b41e3c7..a16642ca79 100644
--- a/contrib/extraction/extraction.ml
+++ b/contrib/extraction/extraction.ml
@@ -481,7 +481,9 @@ and signature_rec env c args =
 	signature_rec env d (Array.to_list args' @ args)
     | Rel n -> 
 	(match lookup_rel n env with
-	   | (_,Some t,_) -> signature_rec env (lift n t) args  
+	   | (_,Some t,_) -> 
+	       let c' = whd_betaiotalet env none (lift n t) in 
+	       signature_rec env c' args
 	   | _ -> [])
     | Const sp when args = [] && is_ml_extraction (ConstRef sp) -> []
     | Const sp when is_axiom sp -> []
@@ -497,7 +499,8 @@ and signature_rec env c args =
 	     | Emlterm _ -> assert false) 
 	else 
 	  let cvalue = constant_value env sp in
-	  signature env (applist (cvalue, args))
+	  let c' = whd_betaiotalet env none (applist (cvalue, args)) in
+	  signature_rec env c' [] 
     | Ind spi ->
 	(match extract_inductive spi with 
 	   |Iml (si,_) -> 
-- 
cgit v1.2.3