diff options
| author | ppedrot | 2013-10-29 19:47:14 +0000 |
|---|---|---|
| committer | ppedrot | 2013-10-29 19:47:14 +0000 |
| commit | 943b5f9a9a90e856171f9dcb13ae56eaa8d87ef0 (patch) | |
| tree | 366dd6d33017f7f00f99ede753585be989f5a9ce /pretyping/reductionops.ml | |
| parent | b8098068f29a58a478efa719c51271d09f66a9d8 (diff) | |
Do not generate useless argument arrays in whd_* functions.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16954 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/reductionops.ml')
| -rw-r--r-- | pretyping/reductionops.ml | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 43e0e99890..8a614d65fd 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -202,8 +202,6 @@ let safe_meta_value sigma ev = try Some (Evd.meta_value sigma ev) with Not_found -> None -let appterm_of_stack t = decompose_app (zip t) - let strong whdfun env sigma t = let rec strongrec env t = map_constr_with_full_binders push_rel strongrec env (whdfun env sigma t) in @@ -551,7 +549,7 @@ let local_whd_state_gen flags sigma = let raw_whd_state_gen flags env sigma s = fst (whd_state_gen false flags env sigma s) let stack_red_of_state_red f sigma x = - appterm_of_stack (f sigma (x, empty_stack)) + decompose_app (zip (f sigma (x, empty_stack))) let red_of_state_red f sigma x = zip (f sigma (x,empty_stack)) @@ -560,6 +558,7 @@ let red_of_state_red f sigma x = let whd_nored_state = local_whd_state_gen nored let whd_nored_stack = stack_red_of_state_red whd_nored_state +let whd_nored = red_of_state_red whd_nored_state (* 1. Beta Reduction Functions *) |