diff options
Diffstat (limited to 'proofs/logic.ml')
-rw-r--r-- | proofs/logic.ml | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/proofs/logic.ml b/proofs/logic.ml index 5c95a8e7a..da62c1036 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -42,9 +42,11 @@ type refiner_error = (* Errors raised by the tactics *) | CannotUnify of constr * constr + | CannotUnifyBindingType of constr * constr | CannotGeneralize of constr | IntroNeedsProduct | DoesNotOccurIn of constr * identifier + | NoOccurrenceFound of constr exception RefinerError of refiner_error |