summaryrefslogtreecommitdiff
path: root/toplevel/classes.ml
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/classes.ml')
-rw-r--r--toplevel/classes.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 435ddb4d..2d8aabfc 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -7,7 +7,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: classes.ml 13332 2010-07-26 22:12:43Z msozeau $ i*)
+(*i $Id: classes.ml 13516 2010-10-07 19:09:38Z msozeau $ i*)
(*i*)
open Names
@@ -233,7 +233,7 @@ let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props
if rest <> [] then
unbound_method env' k.cl_impl (get_id (fst (List.hd rest)))
else
- Inl (type_ctx_instance evars env' k.cl_props props subst)
+ Inl (type_ctx_instance evars (push_rel_context ctx' env') k.cl_props props subst)
in
evars := Evarutil.nf_evar_map !evars;
let term, termtype =