diff options
Diffstat (limited to 'kernel/vmlambda.mli')
| -rw-r--r-- | kernel/vmlambda.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/vmlambda.mli b/kernel/vmlambda.mli index ad5f81638f..03d3393219 100644 --- a/kernel/vmlambda.mli +++ b/kernel/vmlambda.mli @@ -33,7 +33,7 @@ and fix_decl = Name.t Context.binder_annot array * lambda array * lambda array exception TooLargeInductive of Pp.t -val lambda_of_constr : optimize:bool -> env -> Constr.t -> lambda +val lambda_of_constr : optimize:bool -> env -> (existential -> constr option) -> Constr.t -> lambda val decompose_Llam : lambda -> Name.t Context.binder_annot array * lambda |