diff options
Diffstat (limited to 'interp/topconstr.mli')
| -rw-r--r-- | interp/topconstr.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/topconstr.mli b/interp/topconstr.mli index 8f1fa5c3d4..a30c14966a 100644 --- a/interp/topconstr.mli +++ b/interp/topconstr.mli @@ -198,7 +198,7 @@ val coerce_reference_to_id : reference -> identifier val coerce_to_id : constr_expr -> identifier located val coerce_to_name : constr_expr -> name located -val index_of_annot : local_binder list -> identifier located option -> int option +val split_at_annot : local_binder list -> identifier located option -> local_binder list * local_binder list val abstract_constr_expr : constr_expr -> local_binder list -> constr_expr val prod_constr_expr : constr_expr -> local_binder list -> constr_expr |