From d708030189a1c464c110706b5c239e5071a901c9 Mon Sep 17 00:00:00 2001
From: Jasper Hugunin
Date: Wed, 6 Feb 2019 13:21:51 -0800
Subject: Avoid eqn when generating name in induction_gen.

Fixes #9494.
Was failing with "Cannot create self-referring hypothesis" when
the generated name equaled the eqn.
---
 tactics/tactics.ml | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

(limited to 'tactics')

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 070b2356e5..f41706c35e 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -4522,8 +4522,11 @@ let induction_gen clear_flag isrec with_evars elim
      declaring the induction argument as a new local variable *)
     let id =
     (* Type not the right one if partially applied but anyway for internal use*)
+      let avoid = match eqname with
+        | Some {CAst.v=IntroIdentifier id} -> Id.Set.singleton id
+        | _ -> Id.Set.empty in
       let x = id_of_name_using_hdchar env evd t Anonymous in
-      new_fresh_id Id.Set.empty x gl in
+      new_fresh_id avoid x gl in
     let info_arg = (is_arg_pure_hyp, not enough_applied) in
     pose_induction_arg_then
       isrec with_evars info_arg elim id arg t inhyps cls
-- 
cgit v1.2.3