From 61dc740ed1c3780cccaec00d059a28f0d31d0052 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Mon, 4 Jun 2012 12:07:52 +0200 Subject: Imported Upstream version 8.4~gamma0+really8.4beta2 --- proofs/goal.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'proofs/goal.ml') 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 -- cgit v1.2.3