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

1 files changed, 2 insertions, 43 deletions

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 20ada48a1..12aef852d 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -15,7 +15,6 @@ open CErrors
 open Util
 open Names
 open Nameops
-open Term
 open Constr
 open Termops
 open Environ
@@ -1326,46 +1325,6 @@ let index_of_ind_arg sigma t =
       | None -> error "Could not find inductive argument of elimination scheme."
   in aux None 0 t
 
-let enforce_prop_bound_names rename tac =
-  let open Context.Rel.Declaration in
-  match rename with
-  | Some (isrec,nn) when Namegen.use_h_based_elimination_names () ->
-      (* Rename dependent arguments in Prop with name "H" *)
-      (* so as to avoid having hypothesis such as "t:True", "n:~A" when calling *)
-      (* elim or induction with schemes built by Indrec.build_induction_scheme *)
-      let rec aux env sigma i t =
-        if i = 0 then t else match EConstr.kind sigma t with
-        | Prod (Name _ as na,t,t') ->
-            let very_standard = true in
-            let na =
-              if Retyping.get_sort_family_of env sigma t = InProp then
-                (* "very_standard" says that we should have "H" names only, but
-                   this would break compatibility even more... *)
-                let s = match Namegen.head_name sigma t with
-                  | Some id when not very_standard -> Id.to_string id
-                  | _ -> "" in
-                Name (add_suffix Namegen.default_prop_ident s)
-              else
-                na in
-            mkProd (na,t,aux (push_rel (LocalAssum (na,t)) env) sigma (i-1) t')
-        | Prod (Anonymous,t,t') ->
-            mkProd (Anonymous,t,aux (push_rel (LocalAssum (Anonymous,t)) env) sigma (i-1) t')
-        | LetIn (na,c,t,t') ->
-            mkLetIn (na,c,t,aux (push_rel (LocalDef (na,c,t)) env) sigma (i-1) t')
-        | _ -> assert false in
-      let rename_branch i =
-        Proofview.Goal.enter begin fun gl ->
-          let env = Proofview.Goal.env gl in
-          let sigma = Tacmach.New.project gl in
-          let t = Proofview.Goal.concl gl in
-          change_concl (aux env sigma i t)
-        end in
-      (if isrec then Tacticals.New.tclTHENFIRSTn else Tacticals.New.tclTHENLASTn)
-        tac
-        (Array.map rename_branch nn)
-  | _ ->
-      tac
-
 let rec contract_letin_in_lam_header sigma c =
   match EConstr.kind sigma c with
   | Lambda (x,t,c)  -> mkLambda (x,t,contract_letin_in_lam_header sigma c)
@@ -1386,7 +1345,7 @@ let elimination_clause_scheme with_evars ?(with_classes=true) ?(flags=elim_flags
              (str "The type of elimination clause is not well-formed."))
   in
   let elimclause' = clenv_fchain ~flags indmv elimclause indclause in
-  enforce_prop_bound_names rename (Clenvtac.res_pf elimclause' ~with_evars ~with_classes ~flags)
+  Clenvtac.res_pf elimclause' ~with_evars ~with_classes ~flags
   end
 
 (*
@@ -4208,7 +4167,7 @@ let induction_tac with_evars params indvars elim =
   let elimclause' = recolle_clenv i params indvars elimclause gl in
   (* one last resolution (useless?) *)
   let resolved = clenv_unique_resolver ~flags:(elim_flags ()) elimclause' gl in
-  enforce_prop_bound_names rename (Clenvtac.clenv_refine with_evars resolved)
+  Clenvtac.clenv_refine with_evars resolved
   end
 
 (* Apply induction "in place" taking into account dependent