diff options
Diffstat (limited to 'lib/aux_file.ml')
| -rw-r--r-- | lib/aux_file.ml | 4 |
1 files changed, 0 insertions, 4 deletions
diff --git a/lib/aux_file.ml b/lib/aux_file.ml index 17f55330de..1b6651a55f 100644 --- a/lib/aux_file.ml +++ b/lib/aux_file.ml @@ -17,10 +17,6 @@ let version = 1 let oc = ref None -let chop_extension f = - if check_suffix f ".v" then chop_extension f - else f - let aux_file_name_for vfile = dirname vfile ^ "/." ^ chop_extension(basename vfile) ^ ".aux" |