From 562c684cd19c37e04901743c73933ea12148940b Mon Sep 17 00:00:00 2001
From: msozeau
Date: Fri, 9 Oct 2009 22:21:30 +0000
Subject: Fix bug #2162 and a name clashing bug in generalized binders.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12383 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 plugins/subtac/subtac_classes.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'plugins')

diff --git a/plugins/subtac/subtac_classes.ml b/plugins/subtac/subtac_classes.ml
index 6fe14da34d..93b65cd000 100644
--- a/plugins/subtac/subtac_classes.ml
+++ b/plugins/subtac/subtac_classes.ml
@@ -95,7 +95,7 @@ let substitution_of_constrs ctx cstrs =
 let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) pri =
   let env = Global.env() in
   let isevars = ref Evd.empty in
-  let tclass =
+  let tclass, _ =
     match bk with
     | Implicit ->
 	Implicit_quantifiers.implicit_application Idset.empty (* need no avoid *)
@@ -110,7 +110,7 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) p
 		in t, avoid
 	    | None -> failwith ("new instance: under-applied typeclass"))
 	  cl
-      | Explicit -> cl
+      | Explicit -> cl, Idset.empty
   in
   let tclass = if generalize then CGeneralization (dummy_loc, Implicit, Some AbsPi, tclass) else tclass in
   let k, ctx', imps, subst =
-- 
cgit v1.2.3