diff options
author | Stephane Glondu <steph@glondu.net> | 2012-06-04 12:07:52 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2012-06-04 12:07:52 +0200 |
commit | 61dc740ed1c3780cccaec00d059a28f0d31d0052 (patch) | |
tree | d88d05baf35b9b09a034233300f35a694f9fa6c2 /toplevel/classes.ml | |
parent | 97fefe1fcca363a1317e066e7f4b99b9c1e9987b (diff) |
Imported Upstream version 8.4~gamma0+really8.4beta2upstream/8.4_gamma0+really8.4beta2
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); |