From 3dd52dacc7846b85a11f83c398945c00bb65bad2 Mon Sep 17 00:00:00 2001
From: mohring
Date: Tue, 26 Mar 2002 16:29:59 +0000
Subject: Prise en compte des dependances dans la tactique Case

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2567 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/tactics.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'tactics')

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index a300258480..f8b6282703 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1638,7 +1638,9 @@ let general_case_analysis (c,lbindc) gl =
   let (mind,_) = pf_reduce_to_quantified_ind gl (pf_type_of gl c) in
   let sigma    = project gl in 
   let sort     = elimination_sort_of_goal gl in
-  let elim     = Indrec.make_case_gen env sigma mind sort in 
+  let case = if occur_term c (pf_concl gl) then Indrec.make_case_dep
+  else Indrec.make_case_gen in
+  let elim     = case env sigma mind sort in 
   general_elim (c,lbindc) (elim,[]) gl
     
 let simplest_case c = general_case_analysis (c,[])
-- 
cgit v1.2.3