Remove legacy Refiner error constructors.

They were not used anywhere anymore.

3 files changed, 0 insertions, 13 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
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index 4fe3f07d6e..9d67ce3757 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -1112,16 +1112,9 @@ let explain_refiner_cannot_apply env sigma t harg =
   pr_lconstr_env env sigma t ++ spc () ++ str "could not be applied to" ++ brk(1,1) ++
   pr_lconstr_env env sigma harg ++ str "."
 
-let explain_refiner_not_well_typed env sigma c =
-  str "The term " ++ pr_lconstr_env env sigma c ++ str " is not well-typed."
-
 let explain_intro_needs_product () =
   str "Introduction tactics needs products."
 
-let explain_does_not_occur_in env sigma c hyp =
-  str "The term" ++ spc () ++ pr_lconstr_env env sigma c ++ spc () ++
-  str "does not occur in" ++ spc () ++ Id.print hyp ++ str "."
-
 let explain_non_linear_proof env sigma c =
   str "Cannot refine with term" ++ brk(1,1) ++ pr_lconstr_env env sigma c ++
   spc () ++ str "because a metavariable has several occurrences."
@@ -1137,9 +1130,7 @@ let explain_refiner_error env sigma = function
   | BadType (arg,ty,conclty) -> explain_refiner_bad_type env sigma arg ty conclty
   | UnresolvedBindings t -> explain_refiner_unresolved_bindings t
   | CannotApply (t,harg) -> explain_refiner_cannot_apply env sigma t harg
-  | NotWellTyped c -> explain_refiner_not_well_typed env sigma c
   | IntroNeedsProduct -> explain_intro_needs_product ()
-  | DoesNotOccurIn (c,hyp) -> explain_does_not_occur_in env sigma c hyp
   | NonLinearProof c -> explain_non_linear_proof env sigma c
   | MetaInType c -> explain_meta_in_type env sigma c
   | NoSuchHyp id -> explain_no_such_hyp id