diff options
author | Stephane Glondu <steph@glondu.net> | 2012-06-04 12:23:14 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2012-06-04 12:23:14 +0200 |
commit | 86535d84cc3cffeee1dcd8545343f234e7285530 (patch) | |
tree | 9b221c283c2971f7ac151397231059e1d239e723 /plugins/subtac/subtac_pretyping.ml | |
parent | 39efc41237ec906226a3a53d7396d51173495204 (diff) | |
parent | 61dc740ed1c3780cccaec00d059a28f0d31d0052 (diff) |
Remove non-DFSG contentsupstream/8.4_gamma0+really8.4beta2+dfsg
Diffstat (limited to 'plugins/subtac/subtac_pretyping.ml')
-rw-r--r-- | plugins/subtac/subtac_pretyping.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/subtac/subtac_pretyping.ml b/plugins/subtac/subtac_pretyping.ml index 7c0d1232..e56fa4f5 100644 --- a/plugins/subtac/subtac_pretyping.ml +++ b/plugins/subtac/subtac_pretyping.ml @@ -67,8 +67,8 @@ let interp env isevars c tycon = let _ = isevars := Evarutil.nf_evar_map !isevars in let evd = consider_remaining_unif_problems env !isevars in (* let unevd = undefined_evars evd in *) - let unevd' = Typeclasses.resolve_typeclasses ~onlyargs:true ~split:true ~fail:true env evd in - let unevd' = Typeclasses.resolve_typeclasses ~onlyargs:false ~split:true ~fail:false env unevd' in + let unevd' = Typeclasses.resolve_typeclasses ~filter:Subtac_utils.no_goals_or_obligations ~split:true ~fail:true env evd in + let unevd' = Typeclasses.resolve_typeclasses ~filter:Typeclasses.all_evars ~split:true ~fail:false env unevd' in let evm = unevd' in isevars := unevd'; nf_evar evm j.uj_val, nf_evar evm j.uj_type |