From db601b06b0880f573b6d1fa83de471679ce87ee7 Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Wed, 14 Jun 2017 18:18:37 +0200
Subject: plugins/ltac : avoid spurious .cmxs files

 In the previous setting, all plugins/ltac/*.cmxs except ltac_plugin.cmxs
 (for instance coretactics.cmxs, g_auto.cmxs, ...) were utterly bogus :
  - wrong -for-pack used for their inner .cmx
  - dependency over modules not provided (for instance Tacenv, that ends
    up being a submodule of the pack ltac_plugin).
 But we were lucky, those files were actually never loaded, thanks to the
 several DECLARE PLUGIN inside coretactics and co, that end up in ltac_plugin,
 and hence tell Coq that these modules are already known, preventing
 any attempt to load them.

 Anyway, this commit cleans up this mess (thanks PMP for the help)
---
 Makefile.common | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'Makefile.common')

diff --git a/Makefile.common b/Makefile.common
index ec5e6ac855..100698321a 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -134,7 +134,7 @@ OTHERSYNTAXCMO:=$(addprefix plugins/syntax/, \
 	ascii_syntax_plugin.cmo \
         string_syntax_plugin.cmo )
 DERIVECMO:=plugins/derive/derive_plugin.cmo
-LTACCMO:=plugins/ltac/ltac_plugin.cmo
+LTACCMO:=plugins/ltac/ltac_plugin.cmo plugins/ltac/tauto_plugin.cmo
 SSRMATCHINGCMO:=plugins/ssrmatching/ssrmatching_plugin.cmo
 SSRCMO:=plugins/ssr/ssreflect_plugin.cmo
 
-- 
cgit v1.2.3