From bc2c4ee75c2ea96689d42d90872279476bc41b28 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 30 Dec 2009 14:41:01 +0000
Subject: Fixing bug #2193: computation of dependencies in the "match" return
 predicate was incomplete.

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

(limited to 'pretyping')

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 177389c98a..f68bf10c4b 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -835,7 +835,7 @@ let rec map_predicate f k ccl = function
   | Abstract _ :: rest ->
       map_predicate f (k+1) ccl rest
 
-let noccurn_predicate = map_predicate noccurn
+let noccur_predicate_between n = map_predicate (noccur_between n)
 
 let liftn_predicate n = map_predicate (liftn n)
 
@@ -1110,13 +1110,16 @@ let build_branch current deps (realnames,dep) pb arsign eqns const_info =
   (* into  "Gamma; typs; curalias |- tms" *)
   let tomatch = lift_tomatch_stack const_info.cs_nargs pb.tomatch in
 
+  let pred_is_not_dep =
+    noccur_predicate_between 1 (List.length realnames + 1) pb.pred tomatch in
+
   let typs'' =
     list_map2_i
       (fun i (na,t) deps ->
 	let dep = match dep with
 	  | Name _ as na',k -> (if na <> Anonymous then na else na'),k
 	  | Anonymous,KnownNotDep ->
-	      if deps = [] && noccurn_predicate 1 pb.pred tomatch then
+	      if deps = [] && pred_is_not_dep then
 		(Anonymous,KnownNotDep)
 	      else
 		(force_name na,KnownDep)
-- 
cgit v1.2.3