From 57ef36dbdcfe2f5bc47dc1e9dbb1785010d2c151 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 2 Sep 2020 19:31:21 +0200
Subject: Remove a useless use of clenv_fchain in Equality.

The clenv was generated to eliminate a negation, but its argument was given
immediately and its type statically known to be the same.
---
 tactics/equality.ml | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

(limited to 'tactics')

diff --git a/tactics/equality.ml b/tactics/equality.ml
index 535725b11d..7a3467cace 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1049,9 +1049,8 @@ let discr_positions env sigma { eq_data = (lbeq,(t,t1,t2)); eq_clenv = eq_clause
   in
     discriminator >>= fun discriminator ->
     discrimination_pf e (t,t1,t2) discriminator lbeq false_kind >>= fun pf ->
-    let pf_ty = mkArrow (clenv_type eq_clause) Sorts.Relevant false_0 in
-    let absurd_clause = apply_on_clause (pf,pf_ty) eq_clause in
-    let pf = Clenv.clenv_value_cast_meta absurd_clause in
+    (* pf : eq t t1 t2 -> False *)
+    let pf = EConstr.mkApp (pf, [|clenv_value eq_clause|]) in
     tclTHENS (assert_after Anonymous false_0)
       [onLastHypId gen_absurdity; (Logic.refiner ~check:true EConstr.Unsafe.(to_constr pf))]
 
-- 
cgit v1.2.3