Fix #9631: Instance: anomaly grounding non evar-free term

4 files changed, 10 insertions, 12 deletions

diff --git a/vernac/classes.ml b/vernac/classes.ml
index 39c086eff5..306b5d9f0e 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -234,7 +234,7 @@ let do_instance env env' sigma ?hook ~refine ~tac ~global ~poly ~program_mode ct
       in
       match rest with
       | (n, _) :: _ ->
-        unbound_method env' k.cl_impl (get_id n)
+        unbound_method env' sigma k.cl_impl (get_id n)
       | _ ->
         let kcl_props = List.map (Termops.map_rel_decl of_constr) k.cl_props in
         let sigma, res = type_ctx_instance ~program_mode (push_rel_context ctx' env') sigma kcl_props props subst in
diff --git a/vernac/explainErr.ml b/vernac/explainErr.ml
index 06428b53f2..2bc95dbfcd 100644
--- a/vernac/explainErr.ml
+++ b/vernac/explainErr.ml
@@ -64,8 +64,8 @@ let process_vernac_interp_error exn = match fst exn with
       wrap_vernac_error exn (Himsg.explain_pretype_error ctx sigma te)
   | Notation.PrimTokenNotationError(kind,ctx,sigma,te) ->
       wrap_vernac_error exn (Himsg.explain_prim_token_notation_error kind ctx sigma te)
-  | Typeclasses_errors.TypeClassError(env, te) ->
-      wrap_vernac_error exn (Himsg.explain_typeclass_error env te)
+  | Typeclasses_errors.TypeClassError(env, sigma, te) ->
+      wrap_vernac_error exn (Himsg.explain_typeclass_error env sigma te)
   | Implicit_quantifiers.MismatchedContextInstance(e,c,l,x) ->
     wrap_vernac_error exn (Himsg.explain_mismatched_contexts e c l x)
   | InductiveError e ->
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index 9dd321be51..9e92d936d2 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -1039,12 +1039,10 @@ let explain_module_internalization_error = function
 
 (* Typeclass errors *)
 
-let explain_not_a_class env c =
-  let sigma = Evd.from_env env in
-  let c = EConstr.to_constr sigma c in
-  pr_constr_env env sigma c ++ str" is not a declared type class."
+let explain_not_a_class env sigma c =
+  pr_econstr_env env sigma c ++ str" is not a declared type class."
 
-let explain_unbound_method env cid { CAst.v = id } =
+let explain_unbound_method env sigma cid { CAst.v = id } =
   str "Unbound method name " ++ Id.print (id) ++ spc () ++
   str"of class" ++ spc () ++ pr_global cid ++ str "."
 
@@ -1059,9 +1057,9 @@ let explain_mismatched_contexts env c i j =
     fnl () ++ brk (1,1) ++
     hov 1 (str"Found:" ++ brk (1, 1) ++ pr_constr_exprs i)
 
-let explain_typeclass_error env = function
-  | NotAClass c -> explain_not_a_class env c
-  | UnboundMethod (cid, id) -> explain_unbound_method env cid id
+let explain_typeclass_error env sigma = function
+  | NotAClass c -> explain_not_a_class env sigma c
+  | UnboundMethod (cid, id) -> explain_unbound_method env sigma cid id
 
 (* Refiner errors *)
 
diff --git a/vernac/himsg.mli b/vernac/himsg.mli
index f22354cdbf..d0f42ea16b 100644
--- a/vernac/himsg.mli
+++ b/vernac/himsg.mli
@@ -26,7 +26,7 @@ val explain_inductive_error : inductive_error -> Pp.t
 
 val explain_mismatched_contexts : env -> contexts -> Constrexpr.constr_expr list -> Constr.rel_context -> Pp.t
 
-val explain_typeclass_error : env -> typeclass_error -> Pp.t
+val explain_typeclass_error : env -> Evd.evar_map -> typeclass_error -> Pp.t
 
 val explain_recursion_scheme_error : env -> recursion_scheme_error -> Pp.t