Fixing bug #2106 ("match" compilation with multi-dependent constructor).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12167 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 40 insertions, 13 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 70b201a6e5..23b7661829 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -127,7 +127,7 @@ let push_rels vars env = List.fold_right push_rel vars env
 (* We have x1:t1...xn:tn,xi':ti,y1..yk |- c and re-generalize
    over xi:ti to get x1:t1...xn:tn,xi':ti,y1..yk |- c[xi:=xi'] *)
 
-let regeneralize_rel i k j = if j = i+k then k else if j < i+k then j else j
+let regeneralize_rel i k j = if j = i+k then k+1 else j
 
 let rec regeneralize_index i k t = match kind_of_term t with
   | Rel j when j = i+k -> mkRel (k+1)
@@ -591,19 +591,13 @@ let find_dependencies_signature deps_in_rhs typs =
   let _,l = List.fold_right2 find_dependencies deps_in_rhs typs (k,[]) in
   List.map (fun (_,deps,_) -> deps) l
 
-(******)
+(* Assume we had terms t1..tq to match in a context xp:Tp,...,x1:T1 |-
+   and xn:Tn has just been regeneralized into x:Tn so that the terms
+   to match are now to be considered in the context xp:Tp,...,x1:T1,x:Tn |-.
 
-(* A Pushed term to match has just been substituted by some
-   constructor t = (ci x1...xn) and the terms x1 ... xn have been added to
-   match 
-
-   - all terms to match and to push (dependent on t by definition)
-     must have (Rel depth) substituted by t and Rel's>depth lifted by n
-   - all pushed terms to match (non dependent on t by definition) must
-     be lifted by n
-
-  We start with depth=1
-*)
+   [regeneralize_index_tomatch n tomatch] updates t1..tq so that
+   former references to xn are now references to x. Note that t1..tq
+   are already adjusted to the context xp:Tp,...,x1:T1,x:Tn |-. *)
 
 let regeneralize_index_tomatch n =
   let rec genrec depth = function
@@ -644,6 +638,13 @@ let replace_tomatch n c =
       :: replrec (depth+1) rest in
   replrec 0
 
+(* [liftn_tomatch_stack]: a term to match has just been substituted by
+   some constructor t = (ci x1...xn) and the terms x1 ... xn have been
+   added to match; all pushed terms to match must be lifted by n
+   (knowing that [Abstract] introduces a binder in the list of pushed
+   terms to match).
+*)
+
 let rec liftn_tomatch_stack n depth = function
   | [] -> []
   | Pushed ((c,tm),l,dep)::rest ->
diff --git a/test-suite/success/CasesDep.v b/test-suite/success/CasesDep.v
index 49bd77fcd6..63957885c9 100644
--- a/test-suite/success/CasesDep.v
+++ b/test-suite/success/CasesDep.v
@@ -480,3 +480,29 @@ Fixpoint app {A} {n m} (v : listn A n) (w : listn A m) : listn A (n + m) :=
     | niln => w
     | consn a n' v' => consn _ a _ (app v' w)
   end.
+
+(* Testing regression of bug 2106 *)
+
+Set Implicit Arguments.
+Require Import List.
+
+Inductive nt := E.
+Definition root := E.
+Inductive ctor : list nt -> nt -> Type := 
+ Plus : ctor (cons E (cons E nil)) E.
+
+Inductive term : nt -> Type :=
+| Term : forall s n, ctor s n -> spine s -> term n
+with spine : list nt -> Type :=
+| EmptySpine : spine nil
+| ConsSpine : forall n s, term n -> spine s -> spine (n :: s).
+
+Inductive step : nt -> nt -> Type :=
+  | Step : forall l n r n' (c:ctor (l++n::r) n'), spine l -> spine r -> step n
+n'.
+
+Definition test (s:step E E) :=
+  match s with
+    | Step nil _ (cons E nil) _ Plus l l' => true
+    | _ => false
+  end.