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 | |
| 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
| -rw-r--r-- | pretyping/cases.ml | 6 | ||||
| -rw-r--r-- | test-suite/success/CasesDep.v | 12 |
2 files changed, 15 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 diff --git a/test-suite/success/CasesDep.v b/test-suite/success/CasesDep.v index 05554bed7b..d3b7cf3f36 100644 --- a/test-suite/success/CasesDep.v +++ b/test-suite/success/CasesDep.v @@ -48,6 +48,18 @@ Check fun x:{_:{x|x=0}|True}+nat => match x return option nat with | _ => Some 0 end. + (* the next two examples were failing from r14703 (Nov 22 2011) to r14732 *) + (* due to a bug in dependencies postprocessing (revealed by CoLoR) *) + +Check fun x:{x:nat*nat|fst x = 0 & True} => match x return option nat with + | exist2 (x,y) eq_refl I => None + end. + +Check fun x:{_:{x:nat*nat|fst x = 0 & True}|True}+nat => match x return option nat with + | inl (exist (exist2 (x,y) eq_refl I) I) => None + | _ => Some 0 + end. + (* -------------------------------------------------------------------- *) (* Example to test patterns matching on dependent families *) (* This exemple extracted from the developement done by Nacira Chabane *) |