diff options
| author | herbelin | 2011-11-26 21:14:14 +0000 |
|---|---|---|
| committer | herbelin | 2011-11-26 21:14:14 +0000 |
| commit | 4909b386a3e917b184d1872a6745cba4098ae8c5 (patch) | |
| tree | be947a6f6b15d6abaa8eea38429289ca4be25bcd /pretyping | |
| parent | 5c995f9bf8408662c23079e19d1b285ef814e8d9 (diff) | |
Fixed a bug in postprocessing dependencies in pattern-matching compilation
(bug was introduced in r14703 when postprocessing started to traverse
inner cases).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14732 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/cases.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 3060d4bd93..f7421b1ef2 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -1051,8 +1051,8 @@ let rec ungeneralize n ng body = mkApp (ungeneralize n (ng+Array.length args) f,args) | _ -> assert false -let ungeneralize_branch n (sign,body) cs = - (sign,ungeneralize (n+cs.cs_nargs) 0 body) +let ungeneralize_branch n k (sign,body) cs = + (sign,ungeneralize (n+cs.cs_nargs) k body) let postprocess_dependencies evd current brs tomatch pred deps cs = let rec aux k brs tomatch pred tocheck deps = match deps, tomatch with @@ -1071,7 +1071,7 @@ let postprocess_dependencies evd current brs tomatch pred deps cs = let pred = lift_predicate (-1) pred tomatch in let tomatch = relocate_index_tomatch 1 (n+1) tomatch in let tomatch = lift_tomatch_stack (-1) tomatch in - let brs = array_map2 (ungeneralize_branch n) brs cs in + let brs = array_map2 (ungeneralize_branch n k) brs cs in aux k brs tomatch pred tocheck deps | _ -> assert false in aux 0 brs tomatch pred [current] deps |