diff options
Diffstat (limited to 'proofs/logic.ml')
| -rw-r--r-- | proofs/logic.ml | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/proofs/logic.ml b/proofs/logic.ml index b06f16682c..e26733a15d 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -60,10 +60,9 @@ exception RefinerError of refiner_error let catchable_exception = function | Util.UserError _ | TypeError _ | RefinerError _ - | Stdpp.Exc_located(_,(Util.UserError _ | TypeError _ | RefinerError _)) -> - true - | _ -> - false + | Stdpp.Exc_located(_,(Util.UserError _ | TypeError _ | RefinerError _ | + Nametab.GlobalizationError _)) -> true + | _ -> false let error_cannot_unify k (m,n) = raise (RefinerError (CannotUnify (m,n))) |