diff options
| author | herbelin | 2000-10-18 14:37:44 +0000 |
|---|---|---|
| committer | herbelin | 2000-10-18 14:37:44 +0000 |
| commit | bedaec8452d0600ede52efeeac016c9d323c66de (patch) | |
| tree | 7f056ffcd58f58167a0e813d5a8449eb950a8e23 /kernel/reduction.ml | |
| parent | 9983a5754258f74293b77046986b698037902e2b (diff) | |
Renommage canonique :
declaration = definition | assumption
mode de reference = named | rel
Ex:
push_named_decl : named_declaration -> env -> env
lookup_named : identifier -> safe_environment -> constr option * typed_type
add_named_assum : identifier * typed_type -> named_context -> named_context
add_named_def : identifier*constr*typed_type -> named_context -> named_context
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@723 85f007b7-540e-0410-9357-904b9bb8a0f7
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) *) |