From d31cb4d3e55da99d42abdc1f4129ddc03e1631c6 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 12 May 2020 12:02:23 +0200
Subject: Do not use Unsafe.to_constr for old refiner conclusion.

This was useless, since we did not observe the difference on evars.
---
 vernac/himsg.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'vernac')

diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index 41f2ab9c63..4fe3f07d6e 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -1096,7 +1096,7 @@ let explain_typeclass_error env sigma = function
 (* Refiner errors *)
 
 let explain_refiner_bad_type env sigma arg ty conclty =
-  let pm, pn = with_diffs (pr_lconstr_env env sigma ty) (pr_lconstr_env env sigma conclty) in
+  let pm, pn = with_diffs (pr_lconstr_env env sigma ty) (pr_leconstr_env env sigma conclty) in
   str "Refiner was given an argument" ++ brk(1,1) ++
   pr_lconstr_env env sigma arg ++ spc () ++
   str "of type" ++ brk(1,1) ++ pm ++ spc () ++
-- 
cgit v1.2.3


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.
---
 vernac/himsg.ml | 9 ---------
 1 file changed, 9 deletions(-)

(limited to 'vernac')

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