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

6 files changed, 20 insertions, 35 deletions

diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index fec2a92549..7f77bcdba7 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -313,6 +313,12 @@ let occur_var_in_decl env hyp (_,c,typ) =
         occur_var env hyp (body_of_type typ) ||
         occur_var env hyp body
 
+(* Tests that t is a subterm of c *)
+let occur_term t c = 
+  let eq_constr_fail c = if eq_constr t c then raise Occur
+  in let rec occur_rec c = eq_constr_fail c; iter_constr occur_rec c
+  in try occur_rec c; false with Occur -> true
+
 (* returns the list of free debruijn indices in a term *)
 
 let free_rels m = 
diff --git a/pretyping/termops.mli b/pretyping/termops.mli
index c45b1b016c..ebcd93a348 100644
--- a/pretyping/termops.mli
+++ b/pretyping/termops.mli
@@ -67,6 +67,7 @@ val occur_var : env -> identifier -> types -> bool
 val occur_var_in_decl :
   env ->
   identifier -> 'a * types option * types -> bool
+val occur_term : constr -> constr -> bool
 val free_rels : constr -> Intset.t
 
 (* Substitution of metavariables *)
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,[])
diff --git a/theories/Logic/Berardi.v b/theories/Logic/Berardi.v
index b50485d3c7..9f6217320c 100644
--- a/theories/Logic/Berardi.v
+++ b/theories/Logic/Berardi.v
@@ -26,8 +26,6 @@
 }
 >> *)
 
-Require Elimdep.
-
 Set Implicit Arguments.
 
 Section Berardis_paradox.
@@ -51,7 +49,7 @@ Lemma AC_IF : (P,B:Prop)(e1,e2:P)(Q:P->Prop)
 Proof.
 Intros P B e1 e2 Q p1 p2.
 Unfold IFProp.
-Elim (EM B) using or_indd; Assumption.
+Case (EM B); Assumption.
 Qed.
 
 
@@ -82,13 +80,12 @@ Record retract_cond : Prop := {
     inv2: retract -> (a:A)(j2 (i2 a))==a
   }.
 
-Scheme retract_cond_indd := Induction for retract_cond Sort Prop.
 
 (** The dependent elimination above implies the axiom of choice: *)
 Lemma AC: (r:retract_cond) retract -> (a:A)((j2 r) ((i2 r) a))==a.
 Proof.
 Intros r.
-Elim r using retract_cond_indd; Simpl.
+Case r; Simpl.
 Trivial.
 Qed.
 
diff --git a/theories/Logic/Elimdep.v b/theories/Logic/Elimdep.v
deleted file mode 100644
index 98f76fd44c..0000000000
--- a/theories/Logic/Elimdep.v
+++ /dev/null
@@ -1,15 +0,0 @@
-(***********************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
-(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
-(*   \VV/  *************************************************************)
-(*    //   *      This file is distributed under the terms of the      *)
-(*         *       GNU Lesser General Public License Version 2.1       *)
-(***********************************************************************)
-
-(*i $Id$ i*)
-
-(** Dependent elimination of some logical notions. *)
-
-Scheme eq_indd  := Induction for eq  Sort Prop.
-Scheme eqT_indd := Induction for eqT Sort Prop.
-Scheme or_indd  := Induction for or  Sort Prop.
diff --git a/theories/Logic/Eqdep_dec.v b/theories/Logic/Eqdep_dec.v
index 68b0fcbf89..7daff9ba30 100644
--- a/theories/Logic/Eqdep_dec.v
+++ b/theories/Logic/Eqdep_dec.v
@@ -24,8 +24,6 @@
 
 Set Implicit Arguments.
 
-Require Elimdep.
-
   (** Bijection between [eq] and [eqT] *)
   Definition eq2eqT: (A:Set)(x,y:A)x=y->x==y :=
     [A,x,_,eqxy]<[y:A]x==y>Cases eqxy of refl_equal => (refl_eqT ? x) end.
@@ -35,14 +33,12 @@ Require Elimdep.
 
   Lemma eq_eqT_bij: (A:Set)(x,y:A)(p:x=y)p==(eqT2eq (eq2eqT p)).
 Intros.
-Elim p using eq_indd.
-Reflexivity.
+Case p; Reflexivity.
 Save.
 
   Lemma eqT_eq_bij: (A:Set)(x,y:A)(p:x==y)p==(eq2eqT (eqT2eq p)).
 Intros.
-Elim p using eqT_indd.
-Reflexivity.
+Case p; Reflexivity.
 Save.
 
 
@@ -55,8 +51,7 @@ Section DecidableEqDep.
 
   Remark trans_sym_eqT: (x,y:A)(u:x==y)(comp u u)==(refl_eqT ? y).
 Intros.
-Elim u using eqT_indd.
-Trivial.
+Case u; Trivial.
 Save.
 
 
@@ -75,10 +70,10 @@ Save.
   Local nu_constant : (y:A)(u,v:x==y) (nu u)==(nu v).
 Intros.
 Unfold nu.
-Elim (eq_dec x y) using or_indd; Intros.
+Case (eq_dec x y); Intros.
 Reflexivity.
 
-Case b; Trivial.
+Case n; Trivial.
 Save.
 
 
@@ -87,8 +82,7 @@ Save.
 
   Remark nu_left_inv : (y:A)(u:x==y) (nu_inv (nu u))==u.
 Intros.
-Elim u using eqT_indd.
-Unfold nu_inv.
+Case u; Unfold nu_inv.
 Apply trans_sym_eqT.
 Save.
 
@@ -125,12 +119,12 @@ Save.
 Intros.
 Cut (proj (exT_intro A P x y) y)==(proj (exT_intro A P x y') y).
 Simpl.
-Elim (eq_dec x x) using or_indd.
+Case (eq_dec x x).
 Intro e.
 Elim e using K_dec; Trivial.
 
 Intros.
-Case b; Trivial.
+Case n; Trivial.
 
 Case H.
 Reflexivity.