aboutsummaryrefslogtreecommitdiffhomepage
path: root/engine/termops.mli
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-09-09 13:29:28 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-09-09 13:43:42 +0200
commitd55818c7da468ce1c7c9644cb63f68f7561a17bc (patch)
treefc3737cf865b014f5a297ce249b98892e181ecf1 /engine/termops.mli
parent1888527bb43d6a8c801565af3e6376c91769fbc1 (diff)
Tracking careless uses of slow name lookup.
Diffstat (limited to 'engine/termops.mli')
-rw-r--r--engine/termops.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/engine/termops.mli b/engine/termops.mli
index 5d85088f8..0a7ac1f26 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -237,7 +237,7 @@ val map_rel_context_with_binders :
val fold_named_context_both_sides :
('a -> Context.Named.Declaration.t -> Context.Named.Declaration.t list -> 'a) ->
Context.Named.t -> init:'a -> 'a
-val mem_named_context : Id.t -> Context.Named.t -> bool
+val mem_named_context_val : Id.t -> named_context_val -> bool
val compact_named_context : Context.Named.t -> Context.NamedList.t
val compact_named_context_reverse : Context.Named.t -> Context.NamedList.t