diff options
Diffstat (limited to 'plugins/subtac')
| -rw-r--r-- | plugins/subtac/subtac_utils.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/subtac/subtac_utils.ml b/plugins/subtac/subtac_utils.ml index 0beb1e1aea..476724ba6d 100644 --- a/plugins/subtac/subtac_utils.ml +++ b/plugins/subtac/subtac_utils.ml @@ -248,7 +248,7 @@ let build_dependent_sum l = ([intros; (tclTHENSEQ [constructor_tac false (Some 1) 1 - (Rawterm.ImplicitBindings [inj_open (mkVar n)]); + (Rawterm.ImplicitBindings [mkVar n]); cont]); ]))) in |