diff options
Diffstat (limited to 'pretyping/rawterm.mli')
| -rw-r--r-- | pretyping/rawterm.mli | 15 |
1 files changed, 4 insertions, 11 deletions
diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli index d7f8311c79..2498af7b53 100644 --- a/pretyping/rawterm.mli +++ b/pretyping/rawterm.mli @@ -93,19 +93,12 @@ and cases_clauses = cases_clause list val cases_predicate_names : tomatch_tuples -> name list -(* - if PRec (_, names, arities, bodies) is in env then arities are - typed in env too and bodies are typed in env enriched by the - arities incrementally lifted - - [On pourrait plutot mettre les arités aves le type qu'elles auront - dans le contexte servant à typer les body ???] - - - boolean in POldCase means it is recursive - - option in PHole tell if the "?" was apparent or has been implicitely added -*) - val map_rawconstr : (rawconstr -> rawconstr) -> rawconstr -> rawconstr +(* Ensure traversal from left to right *) +val map_rawconstr_left_to_right : + (rawconstr -> rawconstr) -> rawconstr -> rawconstr + (* val map_rawconstr_with_binders_loc : loc -> (identifier -> 'a -> identifier * 'a) -> |