diff options
Diffstat (limited to 'pretyping/rawterm.mli')
| -rw-r--r-- | pretyping/rawterm.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli index 759e0adb6..b56e862ac 100644 --- a/pretyping/rawterm.mli +++ b/pretyping/rawterm.mli @@ -89,11 +89,11 @@ i*) val map_rawconstr : (rawconstr -> rawconstr) -> rawconstr -> rawconstr -(* +(*i val map_rawconstr_with_binders_loc : loc -> (identifier -> 'a -> identifier * 'a) -> ('a -> rawconstr -> rawconstr) -> 'a -> rawconstr -> rawconstr -*) +i*) val occur_rawconstr : identifier -> rawconstr -> bool |