aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools/coqdep_common.ml
diff options
context:
space:
mode:
Diffstat (limited to 'tools/coqdep_common.ml')
-rw-r--r--tools/coqdep_common.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml
index 3dd6cb444..10150497d 100644
--- a/tools/coqdep_common.ml
+++ b/tools/coqdep_common.ml
@@ -427,8 +427,8 @@ let coq_dependencies () =
printf "%s%s%s %s.v.beautified: %s.v" ename !suffixe glob ename ename;
traite_fichier_Coq !suffixe true (name ^ ".v");
printf "\n";
- printf "%s.vi: %s.v" ename ename;
- traite_fichier_Coq ".vi" true (name ^ ".v");
+ printf "%s.vio: %s.v" ename ename;
+ traite_fichier_Coq ".vio" true (name ^ ".v");
printf "\n";
flush stdout)
(List.rev !vAccu)