summaryrefslogtreecommitdiff
path: root/pretyping/cbv.ml
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2009-02-19 13:13:14 +0100
committerGravatar Stephane Glondu <steph@glondu.net>2009-02-19 13:13:14 +0100
commita0a94c1340a63cdb824507b973393882666ba52a (patch)
tree73aa4eb32cbd176379bc91b21c184e2a6882bfe3 /pretyping/cbv.ml
parentcfbfe13f5b515ae2e3c6cdd97e2ccee03bc26e56 (diff)
Imported Upstream version 8.2-1+dfsgupstream/8.2-1+dfsg
Diffstat (limited to 'pretyping/cbv.ml')
-rw-r--r--pretyping/cbv.ml12
1 files changed, 9 insertions, 3 deletions
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)