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 a12c09ec8c..b6ad913f6e 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1307,7 +1307,7 @@ let pf_interp_type ist gl = (* Interprets a reduction expression *) let interp_unfold ist env (l,qid) = - (l,interp_evaluable ist env qid) + (interp_int_or_var_list ist l,interp_evaluable ist env qid) let interp_flag ist env red = { red with rConst = List.map (interp_evaluable ist env) red.rConst } |