From 4ea2825a4589b0c77225dd6f4caf98b12ac6dd6f Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 13 Feb 2020 00:24:58 +0100
Subject: [coqdep] Merge `-sort` and `-suffix` options.

They are always used together, no other use case of `-suffix` that I
can see.
---
 tools/CoqMakefile.in    |  4 ++--
 tools/coqdep.ml         |  3 ---
 tools/coqdep_common.ml  | 10 ++++------
 tools/coqdep_common.mli |  1 -
 4 files changed, 6 insertions(+), 12 deletions(-)

(limited to 'tools')

diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in
index d3ed5e78b4..81ccf2c283 100644
--- a/tools/CoqMakefile.in
+++ b/tools/CoqMakefile.in
@@ -455,13 +455,13 @@ all.ps: $(VFILES)
 	$(SHOW)'COQDOC -ps $(GAL)'
 	$(HIDE)$(COQDOC) \
 		-toc $(COQDOCFLAGS) -ps $(GAL) $(COQDOCLIBS) \
-		-o $@ `$(COQDEP) -sort -suffix .v $(VFILES)`
+		-o $@ `$(COQDEP) -sort $(VFILES)`
 
 all.pdf: $(VFILES)
 	$(SHOW)'COQDOC -pdf $(GAL)'
 	$(HIDE)$(COQDOC) \
 		-toc $(COQDOCFLAGS) -pdf $(GAL) $(COQDOCLIBS) \
-		-o $@ `$(COQDEP) -sort -suffix .v $(VFILES)`
+		-o $@ `$(COQDEP) -sort $(VFILES)`
 
 # FIXME: not quite right, since the output name is different
 gallinahtml: GAL=-g
diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index 950c784325..23cc83b8d3 100644
--- a/tools/coqdep.ml
+++ b/tools/coqdep.ml
@@ -44,7 +44,6 @@ let usage () =
   eprintf "  -vos : also output dependencies about .vos files\n";
   eprintf "  -exclude-dir dir : skip subdirectories named 'dir' during -R/-Q search\n";
   eprintf "  -coqlib dir : set the coq standard library directory\n";
-  eprintf "  -suffix s : \n";
   eprintf "  -slash : deprecated, no effect\n";
   eprintf "  -dyndep (opt|byte|both|no|var) : set how dependencies over ML modules are printed\n";
   exit 1
@@ -81,8 +80,6 @@ let rec parse = function
   | "-exclude-dir" :: [] -> usage ()
   | "-coqlib" :: r :: ll -> Envars.set_user_coqlib r; parse ll
   | "-coqlib" :: [] -> usage ()
-  | "-suffix" :: s :: ll -> suffixe := s ; parse ll
-  | "-suffix" :: [] -> usage ()
   | "-dyndep" :: "no" :: ll -> option_dynlink := No; parse ll
   | "-dyndep" :: "opt" :: ll -> option_dynlink := Opt; parse ll
   | "-dyndep" :: "byte" :: ll -> option_dynlink := Byte; parse ll
diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml
index 5ece595f13..07841abad9 100644
--- a/tools/coqdep_common.ml
+++ b/tools/coqdep_common.ml
@@ -38,8 +38,6 @@ let option_boot = ref false
 
 let norec_dirs = ref StrSet.empty
 
-let suffixe = ref ".vo"
-
 type dir = string option
 
 (** [get_extension f l] checks whether [f] has one of the extensions
@@ -498,10 +496,10 @@ let coq_dependencies () =
   List.iter
     (fun (name,_) ->
        let ename = escape name in
-       let glob = if !option_noglob then "" else " "^ename^".glob" in
+       let glob = if !option_noglob then "" else ename^".glob " in
        let deps = find_dependencies name in
-       printf "%s%s%s %s.v.beautified %s.required_vo: %s.v %s\n" ename !suffixe glob ename ename ename
-        (string_of_dependency_list !suffixe deps);
+       printf "%s.vo %s%s.v.beautified %s.required_vo: %s.v %s\n" ename glob ename ename ename
+        (string_of_dependency_list ".vo" deps);
        printf "%s.vio: %s.v %s\n" ename ename
          (string_of_dependency_list ".vio" deps);
        if !write_vos then
@@ -639,7 +637,7 @@ let sort () =
         done
       with Fin_fichier ->
         close_in cin;
-        printf "%s%s " file !suffixe
+        printf "%s.v " file
     end
   in
   List.iter (fun (name,_) -> loop name) !vAccu
diff --git a/tools/coqdep_common.mli b/tools/coqdep_common.mli
index 1820db4a1e..cb436f7f02 100644
--- a/tools/coqdep_common.mli
+++ b/tools/coqdep_common.mli
@@ -25,7 +25,6 @@ val option_c : bool ref
 val option_noglob : bool ref
 val option_boot : bool ref
 val write_vos : bool ref
-val suffixe : string ref
 
 type dynlink = Opt | Byte | Both | No | Variable
 val option_dynlink : dynlink ref
-- 
cgit v1.2.3