From 9779c0bf4945693bfd37b141e2c9f0fea200ba4d Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 25 Apr 2019 14:09:42 +0200
Subject: Integrate build and documentation of Ltac2

Since Ltac2 cannot be put under the stdlib logical root (some file names
would clash), we move it to the `user-contrib` directory, to avoid adding
another hardcoded path in `coqinit.ml`, following a suggestion by @ejgallego.

Thanks to @Zimmi48 for the thorough documentation review and the
numerous suggestions.
---
 Makefile.common | 9 +++++++--
 1 file changed, 7 insertions(+), 2 deletions(-)

(limited to 'Makefile.common')

diff --git a/Makefile.common b/Makefile.common
index bd0e19cd00..ee3bfb43c5 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -104,10 +104,14 @@ PLUGINDIRS:=\
   rtauto 	nsatz           syntax          btauto \
   ssrmatching	ltac		ssr
 
+USERCONTRIBDIRS:=\
+	Ltac2
+
 SRCDIRS:=\
   $(CORESRCDIRS)  \
   tools 	tools/coqdoc	\
-  $(addprefix plugins/, $(PLUGINDIRS))
+  $(addprefix plugins/, $(PLUGINDIRS))  \
+  $(addprefix user-contrib/, $(USERCONTRIBDIRS))
 
 COQRUN := coqrun
 LIBCOQRUN:=kernel/byterun/lib$(COQRUN).a
@@ -149,13 +153,14 @@ DERIVECMO:=plugins/derive/derive_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
+LTAC2CMO:=user-contrib/Ltac2/ltac2_plugin.cmo
 
 PLUGINSCMO:=$(LTACCMO) $(OMEGACMO) $(MICROMEGACMO) \
         $(RINGCMO) \
         $(EXTRACTIONCMO) \
         $(CCCMO)  $(FOCMO) $(RTAUTOCMO) $(BTAUTOCMO) \
         $(FUNINDCMO) $(NSATZCMO) $(SYNTAXCMO) \
-	$(DERIVECMO) $(SSRMATCHINGCMO) $(SSRCMO)
+	$(DERIVECMO) $(SSRMATCHINGCMO) $(SSRCMO) $(LTAC2CMO)
 
 ifeq ($(HASNATDYNLINK)-$(BEST),false-opt)
  STATICPLUGINS:=$(PLUGINSCMO)
-- 
cgit v1.2.3