diff options
Diffstat (limited to 'tactics/tactics.mli')
| -rw-r--r-- | tactics/tactics.mli | 1 |
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 } |