diff options
| author | herbelin | 2000-09-10 20:37:37 +0000 |
|---|---|---|
| committer | herbelin | 2000-09-10 20:37:37 +0000 |
| commit | e72024e2292a50684b7f280d6efb8fee090e2dbf (patch) | |
| tree | fdba2d8c55f0c74aee8800a0e8c9aec3d3b8a584 /kernel/closure.ml | |
| parent | 583992b6ce38655855f6625a26046ce84c53cdc1 (diff) | |
Suppression de Abst
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@593 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/closure.ml')
| -rw-r--r-- | kernel/closure.ml | 11 |
1 files changed, 5 insertions, 6 deletions
diff --git a/kernel/closure.ml b/kernel/closure.ml index 948361690d..178e5a9de7 100644 --- a/kernel/closure.ml +++ b/kernel/closure.ml @@ -144,7 +144,7 @@ let const_value_cache info c = try Some (Hashtbl.find info.i_tab c) with Not_found -> - match const_abst_opt_value info.i_env info.i_evc c with + match const_evar_opt_value info.i_env info.i_evc c with | Some body -> let v = info.i_repr info body in Hashtbl.add info.i_tab c v; @@ -450,7 +450,6 @@ let rec norm_head info env t stack = (VAL(0, mkProd (x, cbv_norm_term info env t, cbv_norm_term info (subs_lift env) c)), stack) - | IsAbst (_,_) -> failwith "No longer implemented" (* cbv_stack_term performs weak reduction on constr t under the subs * env, with context stack, i.e. ([env]t stack). First computes weak @@ -519,8 +518,8 @@ and apply_stack info t = function apply_stack info (applistc t (List.map (cbv_norm_value info) args)) st | CASE (ty,br,ci,env,st) -> apply_stack info - (mkMutCaseA ci (cbv_norm_term info env ty) t - (Array.map (cbv_norm_term info env) br)) + (mkMutCase (ci, cbv_norm_term info env ty, t, + Array.map (cbv_norm_term info env) br)) st @@ -883,7 +882,7 @@ and whnf_frterm info ft = { norm = uf.norm; term = FLIFT(k, uf) } | FOP2 (Cast,f,_) -> whnf_frterm info f (* remove outer casts *) | FOPN (AppL,appl) -> whnf_apply info appl.(0) (array_tl appl) - | FOPN ((Const _ | Evar _ | Abst _) as op,vars) -> + | FOPN ((Const _ | Evar _) as op,vars) -> if red_under info.i_flags (DELTA op) then let cst = DOPN(op, Array.map term_of_freeze vars) in (match const_value_cache info cst with @@ -953,7 +952,7 @@ and whnf_term info env t = | DOP1 (op, nt) -> { norm = false; term = FOP1 (op, freeze env nt) } | DOP2 (Cast,ct,c) -> whnf_term info env ct (* remove outer casts *) | DOP2 (_,_,_) -> assert false (* Lambda|Prod made explicit *) - | DOPN ((AppL | Const _ | Evar _ | Abst _ | MutCase _) as op, ve) -> + | DOPN ((AppL | Const _ | Evar _ | MutCase _) as op, ve) -> whnf_frterm info { norm = false; term = FOPN (op, freeze_vect env ve) } | DOPN ((MutInd _ | MutConstruct _) as op,v) -> { norm = (v=[||]); term = FOPN (op, freeze_vect env v) } |