diff --git a/Makefile.coq.local b/Makefile.coq.local
index 0635dd131ce..4f167cf518e 100644
--- a/Makefile.coq.local
+++ b/Makefile.coq.local
@@ -31,8 +31,6 @@ ALECTRYON_EXTRAFLAGS ?=
 # setting TIMING=1. By doing so here we get the same effect.
 TIMING ?= 1
 
-ETAGS ?= etags
-
 CATEGORY_VFILES = $(filter theories/Categories%.v, $(VFILES))
 CORE_VFILES = $(filter-out $(CATEGORY_VFILES),$(filter theories/%.v, $(VFILES)))
 CONTRIB_VFILES = $(filter contrib/%.v, $(VFILES))
@@ -242,7 +240,7 @@ dot-file-dep-graphs: $(ALL_DOTFILES)
 # The TAGS file
 TAGS_FILES = $(ALL_VFILES)
 TAGS : $(TAGS_FILES)
-	$(ETAGS) --language=none $(shell cat etc/emacs/etags-args) $^
+	./etc/emacs/run-etags.sh $^
 
 # We separate things to work around `make: execvp: /bin/bash: Argument list too long`
 clean::
diff --git a/dune b/dune
index 0de0fb730de..70098e32031 100644
--- a/dune
+++ b/dune
@@ -55,7 +55,10 @@
  (alias emacs)
  (mode promote)
  (deps
+  etc/emacs/run-etags.sh
   %{bin:etags}
-  (glob_files_rec ./*.v))
+  (:vfile
+   (glob_files_rec theories/*.v)
+   (glob_files_rec contrib/*.v)))
  (action
-  (run etags --language=none %{read:etc/emacs/etags-args} %{deps})))
+  (run etc/emacs/run-etags.sh %{vfile})))
diff --git a/etc/emacs/etags-args b/etc/emacs/etags-args
deleted file mode 100644
index c4b9dbd7fad..00000000000
--- a/etc/emacs/etags-args
+++ /dev/null
@@ -1,2 +0,0 @@
--r '/^[ \t]*\(\(Local\|Global\|Cumulative\|NonCumulative\|Monomorphic\|Polymorphic\|Private\)[ \t]+\)*\(Axiom\|Theorem\|Class\|Instance\|Let\|Ltac\|Definition\|Lemma\|Record\|Remark\|Structure\|Fixpoint\|Fact\|Corollary\|Inductive\|CoInductive\|Proposition\)[ \t]+\([a-zA-Z0-9_'\'']+\)/\4/' 
--r '/^[ \t]*\([a-zA-Z0-9_'\'']+\)[ \t]*:/\1/' 
\ No newline at end of file
diff --git a/etc/emacs/run-etags.sh b/etc/emacs/run-etags.sh
new file mode 100755
index 00000000000..b693697b490
--- /dev/null
+++ b/etc/emacs/run-etags.sh
@@ -0,0 +1,2 @@
+#!/bin/sh
+etags --language=none -r '/^[ \t]*\(\(Local\|Global\|Cumulative\|NonCumulative\|Monomorphic\|Polymorphic\|Private\)[ \t]+\)*\(Axiom\|Theorem\|Class\|Instance\|Let\|Ltac\|Definition\|Lemma\|Record\|Remark\|Structure\|Fixpoint\|Fact\|Corollary\|Inductive\|CoInductive\|Proposition\)[ \t]+\([a-zA-Z0-9_'\'']+\)/\4/' -r '/^[ \t]*\([a-zA-Z0-9_'\'']+\)[ \t]*:/\1/' "$@"