diff options
| author | Pierre-Marie Pédrot | 2020-08-27 16:29:06 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-08-27 16:29:06 +0200 |
| commit | dd7306efc8c3897985913dc7954e553904014ff4 (patch) | |
| tree | 5eb41505bba50ea2b3622d0723cdf75a4bc5c409 /plugins | |
| parent | 2062f9cd5ce3c17c128186d1e9e2193528941e5c (diff) | |
| parent | 2f2c7200c9dd6b2f008989a98cc9a35df8c37300 (diff) | |
Merge PR #12918: tacinterp mini cleanup useless letin
Reviewed-by: ppedrot
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 |