diff options
Diffstat (limited to 'tactics/tacinterp.ml')
| -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 *) |