diff options
| author | Gaëtan Gilbert | 2020-08-27 11:20:29 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-08-27 13:08:44 +0200 |
| commit | 2f2c7200c9dd6b2f008989a98cc9a35df8c37300 (patch) | |
| tree | c87a97df0e6998d0dd0191f40320972e895f716e /plugins | |
| parent | 1797822292e7d81fe3e5b7f76f0ddf4e29d3582c (diff) | |
tacinterp mini cleanup useless letin
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/ltac/tacinterp.ml | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 2ca9a0e69d..88480194c8 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -2125,8 +2125,7 @@ let _ = (* EJGA: We should also pass the proof name if desired, for now poly seems like enough to get reasonable behavior in practice *) - let name, poly = Id.of_string "ltac_gen", poly in - let name, poly = Id.of_string "ltac_gen", poly in + let name = Id.of_string "ltac_gen" in let (c, sigma) = Proof.refine_by_tactic ~name ~poly env sigma ty tac in (EConstr.of_constr c, sigma) in |