From 578ab2e565258caa0f8c20eddde8086011b8f670 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 10 Jun 2008 08:54:43 +0000
Subject: - 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
---
 pretyping/cases.ml | 11 ++++-------
 1 file changed, 4 insertions(+), 7 deletions(-)

(limited to 'pretyping')

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]
-- 
cgit v1.2.3