aboutsummaryrefslogtreecommitdiff
path: root/pretyping/typeclasses.mli
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2016-09-14 11:40:15 +0200
committerPierre-Marie Pédrot2016-09-14 11:40:15 +0200
commit5e4dc9a1896a1dff832089be20cd43f4f4776869 (patch)
treef8661480501f26b7d3dd46e064c1a6084991a280 /pretyping/typeclasses.mli
parent93a03345830047310d975d5de3742fa58a0a224b (diff)
parent3e794be5f02ed438cdc5a351d09bdfb54c0be01a (diff)
Merge branch 'v8.6'
Diffstat (limited to 'pretyping/typeclasses.mli')
-rw-r--r--pretyping/typeclasses.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index 25460ef7d3..2530f5dfae 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -101,7 +101,7 @@ val mark_resolvable : evar_info -> evar_info
val is_class_evar : evar_map -> evar_info -> bool
val is_class_type : evar_map -> types -> bool
-val resolve_typeclasses : ?filter:evar_filter -> ?unique:bool ->
+val resolve_typeclasses : ?fast_path:bool -> ?filter:evar_filter -> ?unique:bool ->
?split:bool -> ?fail:bool -> env -> evar_map -> evar_map
val resolve_one_typeclass : ?unique:bool -> env -> evar_map -> types -> open_constr