diff options
Diffstat (limited to 'proofs/logic.mli')
| -rw-r--r-- | proofs/logic.mli | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/proofs/logic.mli b/proofs/logic.mli index 5381cffc4..a1c525a34 100644 --- a/proofs/logic.mli +++ b/proofs/logic.mli @@ -47,8 +47,10 @@ type refiner_error = (*i Errors raised by the refiner i*) | BadType of constr * constr * constr | OccurMeta of constr + | OccurMetaGoal of constr | CannotApply of constr * constr | NotWellTyped of constr + | NonLinearProof of constr (*i Errors raised by the tactics i*) | CannotUnify of constr * constr |