diff options
| -rw-r--r-- | tactics/tacinterp.ml | 2 | ||||
| -rw-r--r-- | test-suite/success/intros.v | 6 |
2 files changed, 7 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 diff --git a/test-suite/success/intros.v b/test-suite/success/intros.v index 17f160f98e..11156aa0ee 100644 --- a/test-suite/success/intros.v +++ b/test-suite/success/intros.v @@ -78,3 +78,9 @@ intros H2%H%H0. - exact H2. - exact H1. Qed. + +(* Bug found by Enrico *) + +Goal forall x : nat, True. +intros y%(fun x => x). +Abort. |