From b881c53180533ce0757df2b1572f2fa8df042ee8 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 16 Nov 2011 08:46:49 +0000
Subject: Fixing bug #1834 (de Bruijn indices bug in pattern-matching
 compilation).

(technically, since the signature "tomatch" of terms to match and of
terms to generalize is typed in a context that does not consider terms
to match as binders while the return predicate do consider them as
binders, the adjusment of the context of the "tomatch" to the context
of the predicate needs lifting in each missing part of the "tomatch"
context, what was not done)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14664 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/cases.ml | 25 ++++++++++++++-----------
 1 file changed, 14 insertions(+), 11 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 932138f304..a89d5a942c 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -871,20 +871,23 @@ let generalize_predicate (names,(nadep,_)) ny d tms ccl =
 (* where pred is computed by abstract_predicate and PI tms.ccl by            *)
 (* extract_predicate                                                         *)
 (*****************************************************************************)
-let rec extract_predicate l ccl = function
+let rec extract_predicate ccl = function
   | Alias (deppat,nondeppat,_,_)::tms ->
       (* substitution already done in build_branch *)
-      extract_predicate l ccl tms
-  | Abstract d'::tms ->
-      let d' = map_rel_declaration (lift (List.length l)) d' in
-      substl l (mkProd_or_LetIn d' (extract_predicate [] ccl tms))
+      extract_predicate ccl tms
+  | Abstract d::tms ->
+      mkProd_or_LetIn d (extract_predicate ccl tms)
   | Pushed ((cur,NotInd _),_,(dep,_))::tms ->
-      extract_predicate (if dep<>Anonymous then cur::l else l) ccl tms
+      let tms = if dep<>Anonymous then lift_tomatch_stack 1 tms else tms in
+      let pred = extract_predicate ccl tms in
+      if dep<>Anonymous then subst1 cur pred else pred
   | Pushed ((cur,IsInd (_,IndType(_,realargs),_)),_,(dep,_))::tms ->
-      let l = List.rev realargs@l in
-      extract_predicate (if dep<>Anonymous then cur::l else l) ccl tms
+      let k = if dep<>Anonymous then 1 else 0 in
+      let tms = lift_tomatch_stack (List.length realargs + k) tms in
+      let pred = extract_predicate ccl tms in
+      substl (if dep<>Anonymous then cur::realargs else realargs) pred
   | [] ->
-      substl l ccl
+      ccl
 
 let abstract_predicate env sigma indf cur (names,(nadep,_)) tms ccl =
   let sign = make_arity_signature env true indf in
@@ -897,7 +900,7 @@ let abstract_predicate env sigma indf cur (names,(nadep,_)) tms ccl =
       | _ -> (* Initial case *) tms in
   let sign = List.map2 (fun na (_,c,t) -> (na,c,t)) (nadep::names) sign in
   let ccl = if nadep <> Anonymous then ccl else lift_predicate 1 ccl tms in
-  let pred = extract_predicate [] ccl tms in
+  let pred = extract_predicate ccl tms in
   it_mkLambda_or_LetIn_name env pred sign
 
 let known_dependent (_,dep) = (dep = KnownDep)
@@ -1703,7 +1706,7 @@ let prepare_predicate loc typing_fun sigma env tomatchs sign tycon pred =
       let sigma = Option.cata (fun tycon ->
           let na = (Name (id_of_string "x"),KnownNotDep) in
           let tms = List.map (fun tm -> Pushed(tm,[],na)) tomatchs in
-          let predinst = extract_predicate [] predcclj.uj_val tms in
+          let predinst = extract_predicate predcclj.uj_val tms in
           Coercion.inh_conv_coerces_to loc env !evdref predinst tycon)
         !evdref tycon in
       let predccl = (j_nf_evar sigma predcclj).uj_val in
-- 
cgit v1.2.3