diff options
Diffstat (limited to 'kernel/reduction.ml')
| -rw-r--r-- | kernel/reduction.ml | 20 |
1 files changed, 10 insertions, 10 deletions
diff --git a/kernel/reduction.ml b/kernel/reduction.ml index bfb3a565fd..3306927d6e 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -277,7 +277,7 @@ let whd_state_gen flags env sigma = | Some body -> whrec (lift n body, stack) | None -> s) | IsVar id when red_delta flags -> - (match lookup_var_value id env with + (match lookup_named_value id env with | Some body -> whrec (body, stack) | None -> s) *) @@ -975,7 +975,7 @@ let splay_prod env sigma = let t = whd_betadeltaiota env sigma c in match kind_of_term t with | IsProd (n,a,c0) -> - decrec (push_rel_decl (n,outcast_type a) env) + decrec (push_rel_assum (n,outcast_type a) env) ((n,a)::m) c0 | _ -> m,t in @@ -986,8 +986,8 @@ let splay_prod_assum env sigma = let t = whd_betadeltaiota_nolet env sigma c in match kind_of_term c with | IsProd (x,t,c) -> - prodec_rec (push_rel_decl (x,outcast_type t) env) - (Sign.add_rel_decl (x,outcast_type t) l) c + prodec_rec (push_rel_assum (x,outcast_type t) env) + (Sign.add_rel_assum (x,outcast_type t) l) c | IsLetIn (x,b,t,c) -> prodec_rec (push_rel_def (x,b,outcast_type t) env) (Sign.add_rel_def (x,b,outcast_type t) l) c @@ -1009,8 +1009,8 @@ let decomp_n_prod env sigma n = match kind_of_term (whd_betadeltaiota env sigma c) with | IsProd (n,a,c0) -> let a = make_typed_lazy a (fun _ -> Type dummy_univ) in - decrec (push_rel_decl (n,a) env) - (m-1) (Sign.add_rel_decl (n,a) ln) c0 + decrec (push_rel_assum (n,a) env) + (m-1) (Sign.add_rel_assum (n,a) ln) c0 | _ -> error "decomp_n_prod: Not enough products" in decrec env n Sign.empty_rel_context @@ -1078,8 +1078,8 @@ let find_conclusion env sigma = let rec decrec env c = let t = whd_betadeltaiota env sigma c in match kind_of_term t with - | IsProd (x,t,c0) -> decrec (push_rel_decl (x,outcast_type t) env) c0 - | IsLambda (x,t,c0) -> decrec (push_rel_decl (x,outcast_type t) env) c0 + | IsProd (x,t,c0) -> decrec (push_rel_assum (x,outcast_type t) env) c0 + | IsLambda (x,t,c0) -> decrec (push_rel_assum (x,outcast_type t) env) c0 | t -> t in decrec env @@ -1135,12 +1135,12 @@ let poly_args env sigma t = match kind_of_term (whd_betadeltaiota env sigma t) with | IsProd (x,a,b) -> add_free_rels_until n a - (aux (push_rel_decl (x,outcast_type a) env) (n+1) b) + (aux (push_rel_assum (x,outcast_type a) env) (n+1) b) | _ -> Intset.empty in match kind_of_term (whd_betadeltaiota env sigma t) with | IsProd (x,a,b) -> - Intset.elements (aux (push_rel_decl (x,outcast_type a) env) 1 b) + Intset.elements (aux (push_rel_assum (x,outcast_type a) env) 1 b) | _ -> [] (* Expanding existential variables (pretyping.ml) *) |