Merge PR #6899: [compat] Remove "Standard Proposition Elimination"

5 files changed, 2 insertions, 73 deletions

diff --git a/engine/namegen.ml b/engine/namegen.ml
index b1a40aa18..d66b77b57 100644
--- a/engine/namegen.ml
+++ b/engine/namegen.ml
@@ -460,23 +460,3 @@ let rename_bound_vars_as_displayed sigma avoid env c =
     | _ -> c
   in
   rename avoid env c
-
-(**********************************************************************)
-(* "H"-based naming strategy introduced June 2014 for hypotheses in
-   Prop produced by case/elim/destruct/induction, in place of the
-   strategy that was using the first letter of the type, leading to
-   inelegant "n:~A", "e:t=u", etc. when eliminating sumbool or similar
-   types *)
-
-let h_based_elimination_names = ref false
-
-let use_h_based_elimination_names () = !h_based_elimination_names
-
-open Goptions
-
-let _ = declare_bool_option
-	  { optdepr  = true; (* remove in 8.8 *)
-	    optname  = "use of \"H\"-based proposition names in elimination tactics";
-	    optkey   = ["Standard";"Proposition";"Elimination";"Names"];
-	    optread  = (fun () -> !h_based_elimination_names);
-	    optwrite = (:=) h_based_elimination_names }
diff --git a/engine/namegen.mli b/engine/namegen.mli
index 0adbe5a51..1b70ef68d 100644
--- a/engine/namegen.mli
+++ b/engine/namegen.mli
@@ -116,13 +116,6 @@ val compute_displayed_name_in_gen :
   (evar_map -> int -> 'a -> bool) ->
   evar_map -> Id.Set.t -> Name.t -> 'a -> Name.t * Id.Set.t
 
-(**********************************************************************)
-(* Naming strategy for arguments in Prop when eliminating inductive types *)
-
-val use_h_based_elimination_names : unit -> bool
-
-(**********************************************************************)
-
 val set_mangle_names_mode : Id.t -> unit
 (** Turn on mangled names mode and with the given prefix.
     @raise UserError if the argument is invalid as an identifier. *)
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 20ada48a1..12aef852d 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -15,7 +15,6 @@ open CErrors
 open Util
 open Names
 open Nameops
-open Term
 open Constr
 open Termops
 open Environ
@@ -1326,46 +1325,6 @@ let index_of_ind_arg sigma t =
       | None -> error "Could not find inductive argument of elimination scheme."
   in aux None 0 t
 
-let enforce_prop_bound_names rename tac =
-  let open Context.Rel.Declaration in
-  match rename with
-  | Some (isrec,nn) when Namegen.use_h_based_elimination_names () ->
-      (* Rename dependent arguments in Prop with name "H" *)
-      (* so as to avoid having hypothesis such as "t:True", "n:~A" when calling *)
-      (* elim or induction with schemes built by Indrec.build_induction_scheme *)
-      let rec aux env sigma i t =
-        if i = 0 then t else match EConstr.kind sigma t with
-        | Prod (Name _ as na,t,t') ->
-            let very_standard = true in
-            let na =
-              if Retyping.get_sort_family_of env sigma t = InProp then
-                (* "very_standard" says that we should have "H" names only, but
-                   this would break compatibility even more... *)
-                let s = match Namegen.head_name sigma t with
-                  | Some id when not very_standard -> Id.to_string id
-                  | _ -> "" in
-                Name (add_suffix Namegen.default_prop_ident s)
-              else
-                na in
-            mkProd (na,t,aux (push_rel (LocalAssum (na,t)) env) sigma (i-1) t')
-        | Prod (Anonymous,t,t') ->
-            mkProd (Anonymous,t,aux (push_rel (LocalAssum (Anonymous,t)) env) sigma (i-1) t')
-        | LetIn (na,c,t,t') ->
-            mkLetIn (na,c,t,aux (push_rel (LocalDef (na,c,t)) env) sigma (i-1) t')
-        | _ -> assert false in
-      let rename_branch i =
-        Proofview.Goal.enter begin fun gl ->
-          let env = Proofview.Goal.env gl in
-          let sigma = Tacmach.New.project gl in
-          let t = Proofview.Goal.concl gl in
-          change_concl (aux env sigma i t)
-        end in
-      (if isrec then Tacticals.New.tclTHENFIRSTn else Tacticals.New.tclTHENLASTn)
-        tac
-        (Array.map rename_branch nn)
-  | _ ->
-      tac
-
 let rec contract_letin_in_lam_header sigma c =
   match EConstr.kind sigma c with
   | Lambda (x,t,c)  -> mkLambda (x,t,contract_letin_in_lam_header sigma c)
@@ -1386,7 +1345,7 @@ let elimination_clause_scheme with_evars ?(with_classes=true) ?(flags=elim_flags
              (str "The type of elimination clause is not well-formed."))
   in
   let elimclause' = clenv_fchain ~flags indmv elimclause indclause in
-  enforce_prop_bound_names rename (Clenvtac.res_pf elimclause' ~with_evars ~with_classes ~flags)
+  Clenvtac.res_pf elimclause' ~with_evars ~with_classes ~flags
   end
 
 (*
@@ -4208,7 +4167,7 @@ let induction_tac with_evars params indvars elim =
   let elimclause' = recolle_clenv i params indvars elimclause gl in
   (* one last resolution (useless?) *)
   let resolved = clenv_unique_resolver ~flags:(elim_flags ()) elimclause' gl in
-  enforce_prop_bound_names rename (Clenvtac.clenv_refine with_evars resolved)
+  Clenvtac.clenv_refine with_evars resolved
   end
 
 (* Apply induction "in place" taking into account dependent
diff --git a/test-suite/bugs/closed/2378.v b/test-suite/bugs/closed/2378.v
index 85ad41d1c..23a58501f 100644
--- a/test-suite/bugs/closed/2378.v
+++ b/test-suite/bugs/closed/2378.v
@@ -505,8 +505,6 @@ Qed.
 Require Export Coq.Logic.FunctionalExtensionality.
 Print PLanguage.
 
-Unset Standard Proposition Elimination Names.
-
 Program Definition PTransfo l1 l2 (tr: Transformation l1 l2) (h: isSharedTransfo l1 l2 tr): 
 Transformation (PLanguage l1) (PLanguage l2) :=
   mkTransformation (PLanguage l1) (PLanguage l2)
diff --git a/test-suite/bugs/opened/1596.v b/test-suite/bugs/opened/1596.v
index 0b576db6b..820022d99 100644
--- a/test-suite/bugs/opened/1596.v
+++ b/test-suite/bugs/opened/1596.v
@@ -2,7 +2,6 @@ Require Import Relations.
 Require Import FSets.
 Require Import Arith.
 Require Import Omega.
-Unset Standard Proposition Elimination Names.
 
 Set Keyed Unification.