Correction bug #261 + amélioration nommage

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

1 files changed, 6 insertions, 6 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 5c129efa90..a0deab683c 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -641,7 +641,7 @@ let rec find_dependency_list k n = function
   | (used,tdeps,d)::rest -> 
       let deps = find_dependency_list k (n+1) rest in
       if used && dependent_decl (mkRel n) d
-      then list_add_set (k+1-n) (list_union deps tdeps)
+      then list_add_set (List.length rest + 1) (list_union deps tdeps)
       else deps
 
 let find_dependencies is_dep_or_cstr_in_rhs d (k,nextlist) =
@@ -776,12 +776,12 @@ let get_names env sign eqns =
 let recover_alias_names get_name = List.map2 (fun x (_,c,t) ->(get_name x,c,t))
 
 let push_rels_eqn sign eqn =
+  {eqn with rhs = {eqn.rhs with rhs_env = push_rels sign eqn.rhs.rhs_env} }
+
+let push_rels_eqn_with_names sign eqn =
   let pats = List.rev (fst (list_chop (List.length sign) eqn.patterns)) in
   let sign = recover_alias_names alias_of_pat pats sign in
-  {eqn with
-     rhs =
-     {eqn.rhs with
-	rhs_env = push_rels sign eqn.rhs.rhs_env} }
+  push_rels_eqn sign eqn
 
 let build_aliases_context env sigma names allpats pats =
   (* pats is the list of bodies to push as an alias *)
@@ -1314,7 +1314,7 @@ let build_branch current deps pb eqns const_info =
       tomatch = List.rev_append currents tomatch;
       pred = option_app (specialize_predicate (List.rev typs') dep_sign const_info) pb.pred;
       history = history;
-      mat = List.map (push_rels_eqn sign) submat }
+      mat = List.map (push_rels_eqn_with_names sign) submat }
 
 (**********************************************************************
  INVARIANT: