summaryrefslogtreecommitdiff
path: root/toplevel/classes.ml
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2010-10-14 17:51:11 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2010-10-14 17:51:11 +0200
commit3e96002677226c0cdaa8f355938a76cfb37a722a (patch)
tree3ca96e142fdb68e464d2f5f403f315282b94f922 /toplevel/classes.ml
parentf18e6146f4fd6ed5b8ded10a3e602f5f64f919f4 (diff)
Imported Upstream version 8.3upstream/8.3
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 =