diff options
| author | Pierre-Marie Pédrot | 2020-05-12 13:57:50 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-05-12 13:59:18 +0200 |
| commit | 5530ac6ee1fd533a2b56944bd9e16b0d767f3e61 (patch) | |
| tree | d1ccdfcd16c035217cd2963486c71f4cb90dd7db /proofs | |
| parent | 8bc79fd74ff347d93758ca5c088b085f721819fb (diff) | |
Remove legacy Refiner error constructors.
They were not used anywhere anymore.
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 |