From 70e59380e6a6fb6cc5b4685159c2311929bb7b14 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Fri, 18 Nov 2011 10:52:10 +0000
Subject: Fix for subclasses implementation, allowing to register generalized
 classes subclasses during type-checking.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14678 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/typeclasses.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 128d3a6a71..d79310d109 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -241,7 +241,7 @@ let check_instance env sigma c =
 
 let build_subclasses ~check env sigma glob pri =
   let rec aux pri c =
-    let ty = Retyping.get_type_of env sigma c in
+    let ty = Evarutil.nf_evar sigma (Retyping.get_type_of env sigma c) in
       match class_of_constr ty with
       | None -> []
       | Some (rels, (tc, args)) ->
-- 
cgit v1.2.3