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

Ack-by: SkySkimmer
Reviewed-by: ejgallego
Ack-by: ppedrot

1 files changed, 5 insertions, 3 deletions

diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index d732544c5c..1496712bbc 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -124,12 +124,14 @@ let typeclass_univ_instance (cl, u) =
 
 let class_info c =
   try GlobRef.Map.find c !classes
-  with Not_found -> not_a_class (Global.env()) (EConstr.of_constr (printable_constr_of_global c))
+  with Not_found ->
+    let env = Global.env() in
+    not_a_class env (Evd.from_env env) (EConstr.of_constr (printable_constr_of_global c))
 
 let global_class_of_constr env sigma c =
   try let gr, u = Termops.global_of_constr sigma c in
-	class_info gr, u
-  with Not_found -> not_a_class env c
+    GlobRef.Map.find gr !classes, u
+  with Not_found -> not_a_class env sigma c
 
 let dest_class_app env sigma c =
   let cl, args = EConstr.decompose_app sigma c in