From 555c24b7c16a561eac480a64dff0856c8a4313a5 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Sat, 2 Jan 2010 12:31:00 +0000
Subject: Fix bug in last commit, missing a substitution call.

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

diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index a45ab88606..590f5c6f47 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -158,7 +158,7 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true)
       List.fold_right (fun (na, b, t) (args, args') ->
 	match b with
 	| None -> (List.tl args, List.hd args :: args')
-	| Some b -> (args, b :: args'))
+	| Some b -> (args, substl args' b :: args'))
 	(snd cl.cl_context) (args, [])
     in
       cl, c', ctx', ctx, len, imps, args
-- 
cgit v1.2.3