diff options
| -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 *) |