diff options
| author | Hugo Herbelin | 2019-11-14 12:13:20 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-01-30 18:59:26 +0100 |
| commit | 0fde47c049322736bbe8ac46d616c2fa3c59c6dd (patch) | |
| tree | 8fc01047277f2cef812f608ab6dfa8d9e8075a06 /interp | |
| parent | a086919e4bab3fba4469d7374851a2d95021f528 (diff) | |
Constrextern.ml: Move a function earlier to be usable for pattern printing.
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrextern.ml | 18 |
1 files changed, 11 insertions, 7 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 9aa71d0eea..c55e17e7a3 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -281,6 +281,17 @@ let get_extern_reference () = !my_extern_reference let extern_reference ?loc vars l = !my_extern_reference vars l (**********************************************************************) +(* utilities *) + +let rec fill_arg_scopes args subscopes (entry,(_,scopes) as all) = + match args, subscopes with + | [], _ -> [] + | a :: args, scopt :: subscopes -> + (a, (entry, (scopt, scopes))) :: fill_arg_scopes args subscopes all + | a :: args, [] -> + (a, (entry, (None, scopes))) :: fill_arg_scopes args [] all + +(**********************************************************************) (* mapping patterns to cases_pattern_expr *) let add_patt_for_params ind l = @@ -729,13 +740,6 @@ let extern_applied_notation n impl f args = let args = adjust_implicit_arguments false (List.length args) 1 args impl in mkFlattenedCApp (f,args) -let rec fill_arg_scopes args subscopes (entry,(_,scopes) as all) = match args, subscopes with -| [], _ -> [] -| a :: args, scopt :: subscopes -> - (a, (entry, (scopt, scopes))) :: fill_arg_scopes args subscopes all -| a :: args, [] -> - (a, (entry, (None, scopes))) :: fill_arg_scopes args [] all - let extern_args extern env args = let map (arg, argscopes) = lazy (extern argscopes env arg) in List.map map args |