From a0a94c1340a63cdb824507b973393882666ba52a Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Thu, 19 Feb 2009 13:13:14 +0100
Subject: Imported Upstream version 8.2-1+dfsg

---
 pretyping/cbv.ml | 12 +++++++++---
 1 file changed, 9 insertions(+), 3 deletions(-)

(limited to 'pretyping/cbv.ml')

diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml
index 2a01e901..f4c612a5 100644
--- a/pretyping/cbv.ml
+++ b/pretyping/cbv.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: cbv.ml 8802 2006-05-10 20:47:28Z barras $ *)
+(* $Id: cbv.ml 11897 2009-02-09 19:28:02Z barras $ *)
 
 open Util
 open Pp
@@ -218,6 +218,11 @@ let rec norm_head info env t stack =
 		   cbv_norm_term info env' c) in
 	(VAL(0,normt), stack) (* Considérer une coupure commutative ? *)
 
+  | Evar ev ->
+      (match evar_value info ev with
+          Some c -> norm_head info env c stack
+        | None -> (VAL(0, t), stack))
+
   (* non-neutral cases *)
   | Lambda _ ->
       let ctxt,b = decompose_lam t in
@@ -227,7 +232,7 @@ let rec norm_head info env t stack =
   | Construct c -> (CONSTR(c, [||]), stack)
 
   (* neutral cases *)
-  | (Sort _ | Meta _ | Ind _|Evar _) -> (VAL(0, t), stack)
+  | (Sort _ | Meta _ | Ind _) -> (VAL(0, t), stack)
   | Prod (x,t,c) -> 
       (VAL(0, mkProd (x, cbv_norm_term info env t,
 		      cbv_norm_term info (subs_lift env) c)),
@@ -353,8 +358,9 @@ let cbv_norm infos constr =
 type cbv_infos = cbv_value infos
 
 (* constant bodies are normalized at the first expansion *)
-let create_cbv_infos flgs env =
+let create_cbv_infos flgs env sigma =
   create
     (fun old_info c -> cbv_stack_term old_info TOP (ESID 0) c)
     flgs
     env
+    (Reductionops.safe_evar_value sigma)
-- 
cgit v1.2.3