diff options
| -rw-r--r-- | proofs/logic.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/proofs/logic.ml b/proofs/logic.ml index 654bc504a9..74c2a4befc 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -53,7 +53,8 @@ let rec catchable_exception = function (* unification errors *) | PretypeError(_,(CannotUnify _|CannotUnifyLocal _|CannotGeneralize _ |NoOccurrenceFound _|CannotUnifyBindingType _|NotClean _ - |CannotFindWellTypedAbstraction _)) -> true + |CannotFindWellTypedAbstraction _ + |UnsolvableImplicit _)) -> true | _ -> false (* Tells if the refiner should check that the submitted rules do not |