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

2 files changed, 0 insertions, 27 deletions

diff --git a/engine/namegen.ml b/engine/namegen.ml
index b1a40aa18a..d66b77b573 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 0adbe5a51d..1b70ef68dd 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. *)