Remove the elimrename field from Tactics.eliminator.

This is actually dead code, we never observe it.

1 files changed, 0 insertions, 1 deletions

diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 9eb8196280..32c64bacf6 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -282,7 +282,6 @@ val compute_elim_sig : evar_map -> ?elimc:constr with_bindings -> types -> elim_
 (** elim principle with the index of its inductive arg *)
 type eliminator = {
   elimindex : int option;  (** None = find it automatically *)
-  elimrename : (bool * int array) option; (** None = don't rename Prop hyps with H-names *)
   elimbody : constr with_bindings
 }