From 46665f87bbdd2d5fe0c302eae63912d6418d7207 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 22 Feb 2019 17:44:43 +0100
Subject: Fix #9631: Instance: anomaly grounding non evar-free term

---
 pretyping/typeclasses.ml | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

(limited to 'pretyping/typeclasses.ml')

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