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 | |
| parent | 334cbcdffd811135cbc282ef1eace1bc69b0ccbd (diff) | |
Fix bug# 2392
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13515 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | plugins/subtac/subtac_classes.ml | 4 | ||||
| -rw-r--r-- | toplevel/classes.ml | 2 |
2 files changed, 3 insertions, 3 deletions
diff --git a/plugins/subtac/subtac_classes.ml b/plugins/subtac/subtac_classes.ml index a663d3db33..fccb2f9332 100644 --- a/plugins/subtac/subtac_classes.ml +++ b/plugins/subtac/subtac_classes.ml @@ -119,7 +119,7 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) p match props with | Inr term -> let c = interp_casted_constr_evars evars env' term cty in - Inr (c, subst) + Inr c | Inl props -> let get_id = function @@ -159,7 +159,7 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) p let termtype = it_mkProd_or_LetIn ty_constr (ctx' @ ctx) in let term = Termops.it_mkLambda_or_LetIn app (ctx' @ ctx) in term, termtype - | Inr (def, subst) -> + | Inr def -> let termtype = it_mkProd_or_LetIn cty ctx in let term = Termops.it_mkLambda_or_LetIn def ctx in term, termtype 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 = |