From aa21c209f85f37b3d16ff499bbeac15e967bf78f Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Fri, 13 Jan 2017 08:40:17 +0100 Subject: Fix broken .aux machinery. Coq expects aux_file_name_for to give the aux file corresponding to the input file whichever its Coq-related extension, be it .v or .vo or .vio. Commit 3e6fa1c broke this contract when fixing bug #5183. As a consequence, depending on the execution path, Coq would try to save or load from either .foo.aux or .foo.vo.aux or .foo.vio.aux. This commit reverts 3e6fa1c and fixes bug #5183 much earlier in the call chain by not initializing hints when the input file does not end with .v. This also restores 8.5 behavior with respect to aux file naming. --- lib/aux_file.ml | 4 ---- 1 file changed, 4 deletions(-) (limited to 'lib/aux_file.ml') diff --git a/lib/aux_file.ml b/lib/aux_file.ml index 0f0f09aa2..c6c7b4242 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" -- cgit v1.2.3