diff options
| author |  glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-03-04 13:07:44 +0000 |
|---|---|---|
| committer | glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-03-04 13:07:44 +0000 |
| commit | 0389da80801ad7f819db27702e849671185836c4 (patch) | |
| tree | 92dd4910f819241f3e6e5b4c04107bb0cf1c5a0e /checker | |
| parent | 7cf251501d7cc1567630c947de981fb407a773c4 (diff) | |
checker: cleanup
Backport of changes introduced in r13443.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13867 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'checker')
| -rw-r--r-- | checker/closure.ml | 10 | ||||
| -rw-r--r-- | checker/reduction.ml | 2 |
2 files changed, 6 insertions, 6 deletions
diff --git a/checker/closure.ml b/checker/closure.ml index 58c80b521..2227e392e 100644 --- a/checker/closure.ml +++ b/checker/closure.ml @@ -610,15 +610,15 @@ let strip_update_shift_app head stk = let get_nth_arg head n stk = assert (head.norm <> Red); - let rec strip_rec rstk h depth n = function + let rec strip_rec rstk h n = function | Zshift(k) as e :: s -> - strip_rec (e::rstk) (lift_fconstr k h) (depth+k) n s + strip_rec (e::rstk) (lift_fconstr k h) n s | Zapp args::s' -> let q = Array.length args in if n >= q then strip_rec (Zapp args::rstk) - {norm=h.norm;term=FApp(h,args)} depth (n-q) s' + {norm=h.norm;term=FApp(h,args)} (n-q) s' else let bef = Array.sub args 0 n in let aft = Array.sub args (n+1) (q-n-1) in @@ -626,9 +626,9 @@ let get_nth_arg head n stk = List.rev (if n = 0 then rstk else (Zapp bef :: rstk)) in (Some (stk', args.(n)), append_stack aft s') | Zupdate(m)::s -> - strip_rec rstk (update m (h.norm,h.term)) depth n s + strip_rec rstk (update m (h.norm,h.term)) n s | s -> (None, List.rev rstk @ s) in - strip_rec [] head 0 n stk + strip_rec [] head n stk (* Beta reduction: look for an applied argument in the stack. Since the encountered update marks are removed, h must be a whnf *) diff --git a/checker/reduction.ml b/checker/reduction.ml index df3891695..efeaff07f 100644 --- a/checker/reduction.ml +++ b/checker/reduction.ml @@ -208,7 +208,7 @@ let rec ccnv univ cv_pb infos lft1 lft2 term1 term2 = and eqappr univ cv_pb infos (lft1,st1) (lft2,st2) = Util.check_for_interrupt (); (* First head reduce both terms *) - let rec whd_both (t1,stk1) (t2,stk2) = + let rec whd_both (t1,stk1) (t2,stk2) = let st1' = whd_stack infos t1 stk1 in let st2' = whd_stack infos t2 stk2 in (* Now, whd_stack on term2 might have modified st1 (due to sharing), |