- Correction bug 1841 (identificateurs incorrects avec Subclass)

- Correction wish 1866 (un "admit" plus fin dans sa généralisation des hyps)
- Bricoles dans cases.ml


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

1 files changed, 4 insertions, 7 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index ff0ccd21a8..52c8ca4198 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -561,12 +561,13 @@ let dependencies_in_pure_rhs nargs eqns =
   let deps_columns = matrix_transpose deps_rows in
   List.map (List.exists ((=) true)) deps_columns
 
-let dependent_in_decl b d = 
-  fold_rel_declaration (fun c -> (||) (dependent b c)) d false
+let dependent_decl a = function
+  | (na,None,t) -> dependent a t
+  | (na,Some c,t) -> dependent a t || dependent a c
 
 let rec dep_in_tomatch n = function
   | (Pushed _ | Alias _) :: l -> dep_in_tomatch n l
-  | Abstract d :: l -> dependent_in_decl (mkRel n) d or dep_in_tomatch (n+1) l
+  | Abstract d :: l -> dependent_decl (mkRel n) d or dep_in_tomatch (n+1) l
   | [] -> false
 
 let dependencies_in_rhs nargs current tms eqns =
@@ -574,10 +575,6 @@ let dependencies_in_rhs nargs current tms eqns =
   | Rel n when dep_in_tomatch n tms -> list_make nargs true
   | _ -> dependencies_in_pure_rhs nargs eqns
 
-let dependent_decl a = function
-  | (na,None,t) -> dependent a t
-  | (na,Some c,t) -> dependent a t || dependent a c
-
 (* Computing the matrix of dependencies *)
 
 (* We are in context d1...dn |- and [find_dependencies k 1 nextlist]