From c50d7aa6537b46aa0b791cdb28f9dbe66327e6ef Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 3 Sep 2020 12:00:42 +0200
Subject: Inline the last use of apply_on_clause in Equality.

---
 tactics/equality.ml | 19 +++++++++----------
 1 file changed, 9 insertions(+), 10 deletions(-)

diff --git a/tactics/equality.ml b/tactics/equality.ml
index 7a3467cace..88622d153c 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1022,15 +1022,6 @@ type equality = {
 
 let eq_baseid = Id.of_string "e"
 
-let apply_on_clause (f,t) clause =
-  let sigma =  clause.evd in
-  let f_clause = mk_clenv_from_env clause.env sigma None (f,t) in
-  let argmv =
-    (match EConstr.kind sigma (last_arg f_clause.evd f_clause.templval.Evd.rebus) with
-     | Meta mv -> mv
-     | _  -> user_err  (str "Ill-formed clause applicator.")) in
-  clenv_fchain ~with_univs:false argmv f_clause clause
-
 let discr_positions env sigma { eq_data = (lbeq,(t,t1,t2)); eq_clenv = eq_clause } cpath dirn =
   build_coq_True () >>= fun true_0 ->
   build_coq_False () >>= fun false_0 ->
@@ -1405,7 +1396,15 @@ let inject_at_positions env sigma l2r eq posns tac =
       let sigma,congr = Evd.fresh_global env sigma eq.congr in
       let pf = applist(congr,[t;resty;injfun;t1;t2]) in
       let sigma, pf_typ = Typing.type_of env sigma pf in
-      let inj_clause = apply_on_clause (pf,pf_typ) eq_clause in
+      let inj_clause =
+        let sigma = eq_clause.evd in
+        let f_clause = mk_clenv_from_env eq_clause.env sigma None (pf, pf_typ) in
+        let argmv =
+          (match EConstr.kind sigma (last_arg f_clause.evd f_clause.templval.Evd.rebus) with
+          | Meta mv -> mv
+          | _  -> user_err  (str "Ill-formed clause applicator.")) in
+        clenv_fchain ~with_univs:false argmv f_clause eq_clause
+      in
       let pf = Clenv.clenv_value_cast_meta inj_clause in
       let ty = simplify_args env sigma (clenv_type inj_clause) in
         evdref := sigma;
-- 
cgit v1.2.3