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 /proofs/goal.ml | |
| parent | 97fefe1fcca363a1317e066e7f4b99b9c1e9987b (diff) | |
Imported Upstream version 8.4~gamma0+really8.4beta2upstream/8.4_gamma0+really8.4beta2
Diffstat (limited to 'proofs/goal.ml')
| -rw-r--r-- | proofs/goal.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/proofs/goal.ml b/proofs/goal.ml index 1542267e..eeaba76e 100644 --- a/proofs/goal.ml +++ b/proofs/goal.ml @@ -163,8 +163,8 @@ module Refinable = struct (* spiwack: it is not very fine grain since it solves all typeclasses holes, not only those containing the current goal, or a given term. But it seems to fit our needs so far. *) - let resolve_typeclasses ?onlyargs ?split ?(fail=false) () env rdefs _ _ = - rdefs:=Typeclasses.resolve_typeclasses ?onlyargs ?split ~fail env !rdefs; + let resolve_typeclasses ?filter ?split ?(fail=false) () env rdefs _ _ = + rdefs:=Typeclasses.resolve_typeclasses ?filter ?split ~fail env !rdefs; () @@ -563,7 +563,7 @@ module V82 = struct let new_sigma = Evd.add Evd.empty evk new_evi in { Evd.it = build evk ; sigma = new_sigma } - (* Used by the typeclasses *) + (* Used by the compatibility layer and typeclasses *) let nf_evar sigma gl = let evi = content sigma gl in let evi = Evarutil.nf_evar_info sigma evi in |