diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-02-15 18:06:18 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-02-15 18:06:18 +0000 |
| commit | ceba05fb3df673f8378e63c709aff7811014855c (patch) | |
| tree | 141197b03c79b97db581f0e5cfb2c9cb50c0e30d /tactics | |
| 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
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 1bbf87a40..971e0986a 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 *) |