diff options
| author | Hugo Herbelin | 2015-12-10 19:14:19 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2015-12-10 19:15:15 +0100 |
| commit | cdaf8e2ed109bd117da2366a279fa575d7b6185a (patch) | |
| tree | d4b5a0295d4acae7a00a659c9955dde6bac1f545 /tactics | |
| parent | fb77937a6ba0fe45e978911db08de57f931683e1 (diff) | |
Fixing a pat%constr bug. Thanks to Enrico for reporting.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tacinterp.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 693b382cac..59420e4e01 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -866,7 +866,7 @@ and interp_intro_pattern_action ist env sigma = function let sigma,l = interp_intro_pattern_list_as_list ist env sigma l in sigma, IntroInjection l | IntroApplyOn (c,ipat) -> - let c = fun env sigma -> interp_constr ist env sigma c in + let c = fun env sigma -> interp_open_constr ist env sigma c in let sigma,ipat = interp_intro_pattern ist env sigma ipat in sigma, IntroApplyOn (c,ipat) | IntroWildcard | IntroRewrite _ as x -> sigma, x |