diff options
Diffstat (limited to 'pretyping/pretyping.ml')
| -rw-r--r-- | pretyping/pretyping.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index ae87cd8c0..497bde340 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -195,7 +195,7 @@ let _ = (** Miscellaneous interpretation functions *) let interp_universe_level_name evd (loc,s) = let names, _ = Global.global_universe_names () in - if CString.string_contains s "." then + if CString.string_contains ~where:s ~what:"." then match List.rev (CString.split '.' s) with | [] -> anomaly (str"Invalid universe name " ++ str s) | n :: dp -> |