diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/logic.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/proofs/logic.ml b/proofs/logic.ml index ab5b426339..74a1cf7626 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -50,9 +50,9 @@ let catchable_exception = function | Util.UserError _ | TypeError _ | RefinerError _ (* unification errors *) | PretypeError(_,(CannotUnify _|CannotGeneralize _|NoOccurrenceFound _| - CannotUnifyBindingType _)) + CannotUnifyBindingType _|NotClean _)) | Stdpp.Exc_located(_,PretypeError(_,(CannotUnify _|CannotGeneralize _| - NoOccurrenceFound _ | CannotUnifyBindingType _))) + NoOccurrenceFound _ | CannotUnifyBindingType _|NotClean _))) | Stdpp.Exc_located(_,(Util.UserError _ | TypeError _ | RefinerError _ | Nametab.GlobalizationError _ | PretypeError (_,VarNotFound _))) -> true | _ -> false |