From 3e6b64184b66313f2374ce783bc0748419b24de3 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Tue, 26 May 2009 20:36:02 +0000
Subject: Fix de Bruijn lifting bug appearing when we match on multiple terms
 with de Bruijn-bound parameters (reported by W. Swierstra).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12142 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 plugins/subtac/subtac_cases.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/plugins/subtac/subtac_cases.ml b/plugins/subtac/subtac_cases.ml
index 1e5722ef1c..1f20180033 100644
--- a/plugins/subtac/subtac_cases.ml
+++ b/plugins/subtac/subtac_cases.ml
@@ -1734,7 +1734,7 @@ let abstract_tomatch env tomatchs =
 	     Rel n -> (lift lenctx c, lift_tomatch_type lenctx t) :: prev, ctx, names
 	   | _ -> 
 	       let name = next_ident_away_from (id_of_string "filtered_var") names in
-		 (mkRel 1, lift_tomatch_type 1 t) :: lift_ctx 1 prev, 
+		 (mkRel 1, lift_tomatch_type (succ lenctx) t) :: lift_ctx 1 prev, 
 	       (Name name, Some (lift lenctx c), lift lenctx $ type_of_tomatch t) :: ctx, 
 	       name :: names)
       ([], [], []) tomatchs
-- 
cgit v1.2.3