diff options
| -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 b3656c419f..fdafe9a64d 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1107,7 +1107,7 @@ and eval_tactic ist = function | TacArg a -> assert false and interp_ltac_qualid is_applied ist gl (loc,qid as lqid) = - try val_interp ist gl (lookup qid) + try val_interp {lfun=[];lmatch=[];debug=ist.debug} gl (lookup qid) with Not_found -> interp_pure_qualid is_applied (pf_env gl) lqid and interp_ltac_reference isapplied ist gl = function |