aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/implicit_quantifiers.mli
diff options
context:
space:
mode:
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 57eff0b86..0d28eccad 100644
--- a/interp/implicit_quantifiers.mli
+++ b/interp/implicit_quantifiers.mli
@@ -51,4 +51,4 @@ val combine_params_freevar :
val implicit_application : Idset.t -> ?allow_partial:bool ->
(Names.Idset.t -> (global_reference * bool) option * (Names.name * Term.constr option * Term.types) ->
Topconstr.constr_expr * Names.Idset.t) ->
- constr_expr -> constr_expr
+ constr_expr -> constr_expr * Idset.t