diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-11-28 23:23:14 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-11-28 23:23:14 +0000 |
| commit | f0379a9f1e23ebebbb7af67aafa593938324939b (patch) | |
| tree | 0f78a43b29b40dde5b095868d16cecfaf450d937 | |
| parent | 45141987acc8069448a4fe4e0c22af81d3f7f669 (diff) | |
Fixing dependencies postprocessing bug in pattern-matching compilation.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14736 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | pretyping/cases.ml | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index f7421b1ef..f56fb5a42 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -1054,7 +1054,7 @@ let rec ungeneralize n ng 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 postprocess_dependencies evd tocheck brs tomatch pred deps cs = let rec aux k brs tomatch pred tocheck deps = match deps, tomatch with | [], _ -> brs,tomatch,pred,[] | n::deps, Abstract (i,d) :: tomatch -> @@ -1074,7 +1074,7 @@ let postprocess_dependencies evd current brs tomatch pred deps cs = 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 + in aux 0 brs tomatch pred tocheck deps (************************************************************************) (* Sorting equations by constructor *) @@ -1284,8 +1284,9 @@ and match_current pb tomatch = (* We compile branches *) let brvals = array_map2 (compile_branch current realargs (names,dep) deps pb arsign) eqns cstrs in (* We build the (elementary) case analysis *) + let depstocheck = current::binding_vars_of_inductive typ in let brvals,tomatch,pred,inst = - postprocess_dependencies !(pb.evdref) current + postprocess_dependencies !(pb.evdref) depstocheck brvals pb.tomatch pb.pred deps cstrs in let brvals = Array.map (fun (sign,body) -> it_mkLambda_or_LetIn body sign) brvals in |