diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/vernacentries.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 35730eea0..48100aa7f 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1359,7 +1359,7 @@ let _ = declare_int_option { optsync = true; optdepr = false; - optname = "the level of inling duging functor application"; + optname = "the level of inlining during functor application"; optkey = ["Inline";"Level"]; optread = (fun () -> Some (Flags.get_inline_level ())); optwrite = (fun o -> |