diff options
| author | herbelin | 2007-02-15 18:06:18 +0000 |
|---|---|---|
| committer | herbelin | 2007-02-15 18:06:18 +0000 |
| commit | ceba05fb3df673f8378e63c709aff7811014855c (patch) | |
| tree | 141197b03c79b97db581f0e5cfb2c9cb50c0e30d | |
| parent | 2e1e80b173846c8ed7ac94ce5f533ffc6cd6c8bd (diff) | |
Réparation absence d'interprétation des liaisons vers listes
d'occurrences (clause "at") dans ltac
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9648 85f007b7-540e-0410-9357-904b9bb8a0f7
| -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. |