diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/logic.ml | 2 | ||||
| -rw-r--r-- | proofs/logic.mli | 2 |
2 files changed, 0 insertions, 4 deletions
diff --git a/proofs/logic.ml b/proofs/logic.ml index b12d966387..eb0ce23ab7 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -31,13 +31,11 @@ type refiner_error = | BadType of constr * constr * EConstr.t | UnresolvedBindings of Name.t list | CannotApply of constr * constr - | NotWellTyped of constr | NonLinearProof of constr | MetaInType of EConstr.constr (* Errors raised by the tactics *) | IntroNeedsProduct - | DoesNotOccurIn of constr * Id.t | NoSuchHyp of Id.t exception RefinerError of Environ.env * Evd.evar_map * refiner_error diff --git a/proofs/logic.mli b/proofs/logic.mli index e4fed22860..9dc75000a1 100644 --- a/proofs/logic.mli +++ b/proofs/logic.mli @@ -36,13 +36,11 @@ type refiner_error = | BadType of constr * constr * EConstr.t | UnresolvedBindings of Name.t list | CannotApply of constr * constr - | NotWellTyped of constr | NonLinearProof of constr | MetaInType of EConstr.constr (*i Errors raised by the tactics i*) | IntroNeedsProduct - | DoesNotOccurIn of constr * Id.t | NoSuchHyp of Id.t exception RefinerError of Environ.env * evar_map * refiner_error |