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 /toplevel/classes.ml | |
parent | 39efc41237ec906226a3a53d7396d51173495204 (diff) | |
parent | 61dc740ed1c3780cccaec00d059a28f0d31d0052 (diff) |
Remove non-DFSG contentsupstream/8.4_gamma0+really8.4beta2+dfsg
Diffstat (limited to 'toplevel/classes.ml')
-rw-r--r-- | toplevel/classes.ml | 9 |
1 files changed, 8 insertions, 1 deletions
diff --git a/toplevel/classes.ml b/toplevel/classes.ml index 1e83e4b8..18f12582 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -252,6 +252,14 @@ let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props let term = Termops.it_mkLambda_or_LetIn def ctx in Some term, termtype in + let _ = + evars := Evarutil.nf_evar_map !evars; + evars := Typeclasses.resolve_typeclasses ~filter:Typeclasses.no_goals ~fail:true + env !evars; + (* Try resolving fields that are typeclasses automatically. *) + evars := Typeclasses.resolve_typeclasses ~filter:Typeclasses.all_evars ~fail:false + env !evars + in let termtype = Evarutil.nf_evar !evars termtype in let term = Option.map (Evarutil.nf_evar !evars) term in let evm = undefined_evars !evars in @@ -259,7 +267,6 @@ let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props if Evd.is_empty evm && term <> None then declare_instance_constant k pri global imps ?hook id (Option.get term) termtype else begin - evars := Typeclasses.resolve_typeclasses ~onlyargs:true ~fail:true env !evars; let kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Instance in Flags.silently (fun () -> Lemmas.start_proof id kind termtype (fun _ -> instance_hook k pri global imps ?hook); |