diff options
Diffstat (limited to 'contrib/subtac/subtac_utils.ml')
| -rw-r--r-- | contrib/subtac/subtac_utils.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/subtac/subtac_utils.ml b/contrib/subtac/subtac_utils.ml index dc79597dd4..91bf626b10 100644 --- a/contrib/subtac/subtac_utils.ml +++ b/contrib/subtac/subtac_utils.ml @@ -238,7 +238,7 @@ let build_dependent_sum l = (tclTHENS tac ([intros; (tclTHENSEQ - [constructor_tac (Some 1) 1 + [constructor_tac false (Some 1) 1 (Rawterm.ImplicitBindings [inj_open (mkVar n)]); cont]); ]))) |