diff options
Diffstat (limited to 'pretyping/cbv.ml')
| -rw-r--r-- | pretyping/cbv.ml | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml index 88f59ded..33166ba8 100644 --- a/pretyping/cbv.ml +++ b/pretyping/cbv.ml @@ -6,16 +6,16 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: cbv.ml,v 1.12.2.1 2004/07/16 19:30:44 herbelin Exp $ *) +(* $Id: cbv.ml 7639 2005-12-02 10:01:15Z gregoire $ *) open Util open Pp open Term open Names open Environ -open Instantiate open Univ open Evd +open Conv_oracle open Closure open Esubst @@ -92,7 +92,7 @@ let contract_cofixp env (i,(_,_,bds as bodies)) = subst_bodies_from_i 0 env, bds.(i) let make_constr_ref n = function - | FarRelKey p -> mkRel (n+p) + | RelKey p -> mkRel (n+p) | VarKey id -> mkVar id | ConstKey cst -> mkConst cst @@ -128,7 +128,7 @@ let stack_app appl stack = open RedFlags let red_set_ref flags = function - | FarRelKey _ -> red_set flags fDELTA + | RelKey _ -> red_set flags fDELTA | VarKey id -> red_set flags (fVAR id) | ConstKey sp -> red_set flags (fCONST sp) @@ -186,7 +186,7 @@ let rec norm_head info env t stack = let nargs = Array.map (cbv_stack_term info TOP env) args in norm_head info env head (stack_app (Array.to_list nargs) stack) | Case (ci,p,c,v) -> norm_head info env c (CASE(p,v,ci,env,stack)) - | Cast (ct,_) -> norm_head info env ct stack + | Cast (ct,_,_) -> norm_head info env ct stack (* constants, axioms * the first pattern is CRUCIAL, n=0 happens very often: @@ -196,7 +196,7 @@ let rec norm_head info env t stack = | Inl (0,v) -> strip_appl v stack | Inl (n,v) -> strip_appl (shift_value n v) stack | Inr (n,None) -> (VAL(0, mkRel n), stack) - | Inr (n,Some p) -> norm_head_ref (n-p) info env stack (FarRelKey p)) + | Inr (n,Some p) -> norm_head_ref (n-p) info env stack (RelKey p)) | Var id -> norm_head_ref 0 info env stack (VarKey id) |