diff options
| author |  Stephane Glondu <steph@glondu.net> | 2009-02-19 13:13:14 +0100 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2009-02-19 13:13:14 +0100 |
| commit | a0a94c1340a63cdb824507b973393882666ba52a (patch) | |
| tree | 73aa4eb32cbd176379bc91b21c184e2a6882bfe3 /pretyping/cbv.ml | |
| parent | cfbfe13f5b515ae2e3c6cdd97e2ccee03bc26e56 (diff) | |
Imported Upstream version 8.2-1+dfsgupstream/8.2-1+dfsg
Diffstat (limited to 'pretyping/cbv.ml')
| -rw-r--r-- | pretyping/cbv.ml | 12 |
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) |