diff options
| author | msozeau | 2010-10-07 18:37:44 +0000 |
|---|---|---|
| committer | msozeau | 2010-10-07 18:37:44 +0000 |
| commit | ad31926a8a97ebf41f700feee0194b294474a791 (patch) | |
| tree | 1eedab59857d4c2d4f7da9198b7916f5c008145e /toplevel | |
| parent | 334cbcdffd811135cbc282ef1eace1bc69b0ccbd (diff) | |
Fix bug# 2392
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13515 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/classes.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/classes.ml b/toplevel/classes.ml index 9418a4a5e6..bf029f4190 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -223,7 +223,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 = |