diff options
| -rw-r--r-- | tactics/tacinterp.ml | 2 | ||||
| -rw-r--r-- | test-suite/success/ltac.v | 10 |
2 files changed, 11 insertions, 1 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 1bbf87a40b..971e0986ae 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1188,7 +1188,7 @@ let interp_hyp_location ist gl ((occs,id),hl) = let interp_clause ist gl { onhyps=ol; onconcl=b; concl_occs=occs } = { onhyps=option_map(List.map (interp_hyp_location ist gl)) ol; onconcl=b; - concl_occs=occs } + concl_occs= interp_int_or_var_list ist occs } (* Interpretation of constructions *) diff --git a/test-suite/success/ltac.v b/test-suite/success/ltac.v index 05a6a70f39..880b5da11f 100644 --- a/test-suite/success/ltac.v +++ b/test-suite/success/ltac.v @@ -188,3 +188,13 @@ Ltac to_exist := Goal forall x y : nat, x = y. to_exist. exact (fun H => H). Abort. + +(* Used to fail in V8.1 *) + +Tactic Notation "test" constr(t) integer(n) := + set (k := t) in |- * at n. + +Goal forall x : nat, x = 1 -> x + x + x = 3. +intros x H. +test x 2. +Abort. |