aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/implicit_quantifiers.mli
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2017-02-02 18:21:51 +0100
committerGravatar Maxime Dénès <mail@maximedenes.fr>2017-03-24 12:17:35 +0100
commit4e4fb7bd42364fd623f8e0e0d3007cd79d78764b (patch)
tree42dfb8c1b0d8db6b3c70da6d093de9b4fec2385c /interp/implicit_quantifiers.mli
parent68ffb813a0e1c7d62dac4769d0104210c2e5f6e9 (diff)
Renaming local_binder into local_binder_expr.
This is a bit long, but it is to keep a symmetry with constr_expr.
Diffstat (limited to 'interp/implicit_quantifiers.mli')
-rw-r--r--interp/implicit_quantifiers.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli
index d0327e506..71009ec3c 100644
--- a/interp/implicit_quantifiers.mli
+++ b/interp/implicit_quantifiers.mli
@@ -25,7 +25,7 @@ val free_vars_of_constr_expr : constr_expr -> ?bound:Id.Set.t ->
Id.t list -> Id.t list
val free_vars_of_binders :
- ?bound:Id.Set.t -> Id.t list -> local_binder list -> Id.Set.t * Id.t list
+ ?bound:Id.Set.t -> Id.t list -> local_binder_expr list -> Id.Set.t * Id.t list
(** Returns the generalizable free ids in left-to-right
order with the location of their first occurrence *)