diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2018-03-08 11:17:14 +0100 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2018-03-08 11:17:14 +0100 |
commit | 76058420ec0ea037504adf0af213d0542bd7c1c3 (patch) | |
tree | 37282697132f0b7db4f560b5503f7ec2dba11029 /engine/namegen.ml | |
parent | 1f5699d57e9d4950b43d6c5f5259c3cf15564b31 (diff) | |
parent | 34babfdb5f45a04e89f671a21cc632ad127a26d4 (diff) |
Merge PR #6899: [compat] Remove "Standard Proposition Elimination"
Diffstat (limited to 'engine/namegen.ml')
-rw-r--r-- | engine/namegen.ml | 20 |
1 files changed, 0 insertions, 20 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 } |