diff options
| author | herbelin | 2009-12-30 14:41:01 +0000 |
|---|---|---|
| committer | herbelin | 2009-12-30 14:41:01 +0000 |
| commit | bc2c4ee75c2ea96689d42d90872279476bc41b28 (patch) | |
| tree | b35a03831232c71e14a4b8cac33aa753f93eb438 /pretyping | |
| parent | 306d1be283442c361aa26d000d339f3f4dfbeab9 (diff) | |
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
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/cases.ml | 7 |
1 files changed, 5 insertions, 2 deletions
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) |