From 5530ac6ee1fd533a2b56944bd9e16b0d767f3e61 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 12 May 2020 13:57:50 +0200
Subject: Remove legacy Refiner error constructors.

They were not used anywhere anymore.
---
 proofs/logic.ml  | 2 --
 proofs/logic.mli | 2 --
 2 files changed, 4 deletions(-)

(limited to 'proofs')

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
-- 
cgit v1.2.3