diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tacinterp.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 3012cbae2f..1450d50322 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -2982,7 +2982,9 @@ let globTacticIn t = TacArg (TacDynamic (dummy_loc,tactic_in t)) let tacticIn t = globTacticIn (fun ist -> try glob_tactic (t ist) - with e -> raise (AnomalyOnError ("Incorrect tactic expression", e))) + with e -> anomalylabstrm "tacticIn" + (str "Incorrect tactic expression. Received exception is:" ++ + Errors.print e)) let tacticOut = function | TacArg (TacDynamic (_,d)) -> |