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.mli | |
| parent | 97fefe1fcca363a1317e066e7f4b99b9c1e9987b (diff) | |
Imported Upstream version 8.4~gamma0+really8.4beta2upstream/8.4_gamma0+really8.4beta2
Diffstat (limited to 'proofs/goal.mli')
| -rw-r--r-- | proofs/goal.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/proofs/goal.mli b/proofs/goal.mli index e9d23065..50709555 100644 --- a/proofs/goal.mli +++ b/proofs/goal.mli @@ -72,7 +72,7 @@ module Refinable : sig (* [with_type c typ] constrains term [c] to have type [typ]. *) val with_type : Term.constr -> Term.types -> Term.constr sensitive - val resolve_typeclasses : ?onlyargs:bool -> ?split:bool -> ?fail:bool -> unit -> unit sensitive + val resolve_typeclasses : ?filter:(Evd.hole_kind -> bool) -> ?split:bool -> ?fail:bool -> unit -> unit sensitive (* [constr_of_raw h check_type resolve_classes] is a pretyping function. @@ -234,7 +234,7 @@ module V82 : sig (* Used for congruence closure *) val new_goal_with : Evd.evar_map -> goal -> Environ.named_context_val -> goal Evd.sigma - (* Used by the typeclasses *) + (* Used by the compatibility layer and typeclasses *) val nf_evar : Evd.evar_map -> goal -> goal * Evd.evar_map (* Goal represented as a type, doesn't take into account section variables *) |