diff options
| author | Pierre-Marie Pédrot | 2020-09-02 19:31:21 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-09-04 22:48:15 +0200 |
| commit | 57ef36dbdcfe2f5bc47dc1e9dbb1785010d2c151 (patch) | |
| tree | 1c45599ebc67c64f405a729e56899f435ae14860 /tactics | |
| parent | 99a9e6b938e8d9237779d384bc8295c1f30cbdce (diff) | |
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.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/equality.ml | 5 |
1 files changed, 2 insertions, 3 deletions
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))] |