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 /plugins | |
| 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 'plugins')
| -rw-r--r-- | plugins/subtac/subtac_classes.ml | 4 |
1 files changed, 2 insertions, 2 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 |