diff options
Diffstat (limited to 'plugins/extraction/mlutil.mli')
| -rw-r--r-- | plugins/extraction/mlutil.mli | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/plugins/extraction/mlutil.mli b/plugins/extraction/mlutil.mli index e8fa9c47b7..452fd46c00 100644 --- a/plugins/extraction/mlutil.mli +++ b/plugins/extraction/mlutil.mli @@ -113,9 +113,11 @@ val normalize : ml_ast -> ml_ast val optimize_fix : ml_ast -> ml_ast val inline : global_reference -> ml_ast -> bool +val is_basic_pattern : ml_pattern -> bool +val has_deep_pattern : ml_branch array -> bool +val is_regular_match : ml_branch array -> bool + exception Impossible -val branch_as_fun : ml_type list -> ml_branch -> ml_ast -val branch_as_cst : ml_branch -> ml_ast (* Classification of signatures *) |