diff options
| -rw-r--r-- | tactics/tacinterp.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 0a219ddc9e..1bebcec498 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1101,8 +1101,8 @@ let rec val_interp ist ast = value_interp ist and eval_tactic ist = function - | TacAtom (loc,t) -> - (try interp_atomic ist t + | TacAtom (loc,t) -> fun gl -> + (try interp_atomic ist t gl with e -> Stdpp.raise_with_loc loc e) | TacFun (it,body) -> assert false | TacFunRec rc -> assert false |