diff --git a/src/plugins/wp/share/Makefile b/src/plugins/wp/share/Makefile
index c4adc837f46a4ccf1f637fef636155f891c86489..6f2822825dd825475ed80058a402d03e84071705 100644
--- a/src/plugins/wp/share/Makefile
+++ b/src/plugins/wp/share/Makefile
@@ -53,6 +53,10 @@ $(WPLSHARE)/why3/%.vo: $(WPLSHARE)/why3/%.v
 	echo "Coqc         $@"
 	@coqc -w none $(WHY3INCLUDES) $<
 
+$(WPLSHARE)/why3/%.ide: $(WPLSHARE)/why3/%.v
+	echo "Coqide       $@"
+	@coqide $(WHY3INCLUDES) $<
+
 $(WPLSHARE)/why3/.depend: $(addprefix $(WPLSHARE)/, $(WHY3_COQ_SOURCES))
 	echo "Coqdep for $(WPLSHARE)/why3"
 	@coqdep $(WHY3INCLUDES) $(WPLSHARE)/why3/*.v $(WPLSHARE)/why3/**/*.v > $@
@@ -84,6 +88,10 @@ $(WPLSHARE)/coqwp/%.vo: $(WPLSHARE)/coqwp/%.v
 	echo "Coqc         $<"
 	coqc -w none $(COQWPINCLUDES) $<
 
+$(WPLSHARE)/coqwp/%.ide: $(WPLSHARE)/coqwp/%.v
+	echo "Coqide       $<"
+	coqide $(COQWPINCLUDES) $<
+
 $(WPLSHARE)/coqwp/.depend: $(addprefix $(WPLSHARE)/, $(WP_COQ_SOURCES))
 	echo "Coqdep for $(WPLSHARE)/coqwp"
 	@coqdep $(COQWPINCLUDES) $(WPLSHARE)/coqwp/*.v $(WPLSHARE)/coqwp/**/*.v > $@