From f0379a9f1e23ebebbb7af67aafa593938324939b Mon Sep 17 00:00:00 2001 From: herbelin Date: Mon, 28 Nov 2011 23:23:14 +0000 Subject: 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 --- pretyping/cases.ml | 7 ++++--- 1 file 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 -- cgit v1.2.3