Remove deprecated option Dependent Propositions Eliminiation.

And a bit of code simplification.

1 files changed, 6 insertions, 22 deletions

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index e072bd95f..cc5593f3f 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -59,20 +59,6 @@ let typ_of env sigma c =
 
 open Goptions
 
-(* Option for 8.2 compatibility *)
-let dependent_propositions_elimination = ref true
-
-let use_dependent_propositions_elimination () =
-  !dependent_propositions_elimination
-
-let _ =
-  declare_bool_option
-    { optdepr  = true; (* remove in 8.8 *)
-      optname  = "dependent-propositions-elimination tactic";
-      optkey   = ["Dependent";"Propositions";"Elimination"];
-      optread  = (fun () -> !dependent_propositions_elimination) ;
-      optwrite = (fun b -> dependent_propositions_elimination := b) }
-
 let _ =
   declare_bool_option
     { optdepr  = true; (* remove in 8.8 *)
@@ -4141,8 +4127,7 @@ let guess_elim isrec dep s hyp0 gl =
       let env = Tacmach.New.pf_env gl in
       let sigma = Tacmach.New.project gl in
       let u = EInstance.kind (Tacmach.New.project gl) u in
-      if use_dependent_propositions_elimination () && dep = Some true
-      then
+      if dep then
         let (sigma, ind) = build_case_analysis_scheme env sigma (mind, u) true s in
         let ind = EConstr.of_constr ind in
         (sigma, ind)
@@ -4174,11 +4159,10 @@ let find_induction_type isrec elim hyp0 gl =
     match elim with
     | None ->
        let sort = Tacticals.New.elimination_sort_of_goal gl in
-       let _, (elimc,elimt),_ = 
-	 guess_elim isrec None sort hyp0 gl in
-	let scheme = compute_elim_sig sigma ~elimc elimt in
-	(* We drop the scheme waiting to know if it is dependent *)
-	scheme, ElimOver (isrec,hyp0)
+       let _, (elimc,elimt),_ = guess_elim isrec false sort hyp0 gl in
+       let scheme = compute_elim_sig sigma ~elimc elimt in
+       (* We drop the scheme waiting to know if it is dependent *)
+       scheme, ElimOver (isrec,hyp0)
     | Some e ->
 	let evd, (elimc,elimt),ind_guess = given_elim hyp0 e gl in
 	let scheme = compute_elim_sig sigma ~elimc elimt in
@@ -4209,7 +4193,7 @@ let get_eliminator elim dep s gl =
   | ElimUsing (elim,indsign) ->
       Tacmach.New.project gl, (* bugged, should be computed *) true, elim, indsign
   | ElimOver (isrec,id) ->
-      let evd, (elimc,elimt),_ as elims = guess_elim isrec (Some dep) s id gl in
+      let evd, (elimc,elimt),_ as elims = guess_elim isrec dep s id gl in
       let _, (l, s) = compute_elim_signature elims id in
       let branchlengthes = List.map (fun d -> assert (RelDecl.is_local_assum d); pi1 (decompose_prod_letin (Tacmach.New.project gl) (RelDecl.get_type d)))
                                     (List.rev s.branches)