From 653de32139ecee3114779a5ee2961c58793889e5 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Thu, 6 Oct 2016 16:59:27 +0200
Subject: Ltac as a plugin.

This commit is essentially moving files around. In particular, the corresponding
plugin still relies on a mllib file rather than a mlpack one. Otherwise, this
causes link-time issues for third-party plugins depending on modules defined
in the Ltac plugin.
---
 Makefile.dev | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

(limited to 'Makefile.dev')

diff --git a/Makefile.dev b/Makefile.dev
index 8c1812da1..ea6b8b919 100644
--- a/Makefile.dev
+++ b/Makefile.dev
@@ -121,10 +121,9 @@ pretyping: pretyping/pretyping.cma
 highparsing: parsing/highparsing.cma
 stm: stm/stm.cma
 toplevel: toplevel/toplevel.cma
-ltac: ltac/ltac.cma
 
 .PHONY: lib kernel byterun library proofs tactics interp parsing pretyping
-.PHONY: engine highparsing stm toplevel ltac
+.PHONY: engine highparsing stm toplevel
 
 ######################
 ### 3) theories files
@@ -183,6 +182,7 @@ RTAUTOVO:=$(filter plugins/rtauto/%, $(PLUGINSVO))
 EXTRACTIONVO:=$(filter plugins/extraction/%, $(PLUGINSVO))
 CCVO:=
 DERIVEVO:=$(filter plugins/derive/%, $(PLUGINSVO))
+LTACVO:=$(filter plugins/ltac/%, $(PLUGINSVO))
 
 omega: $(OMEGAVO) $(OMEGACMO) $(ROMEGAVO) $(ROMEGACMO)
 micromega: $(MICROMEGAVO) $(MICROMEGACMO) $(CSDPCERT)
@@ -194,9 +194,10 @@ funind: $(FUNINDCMO) $(FUNINDVO)
 cc: $(CCVO) $(CCCMO)
 rtauto: $(RTAUTOVO) $(RTAUTOCMO)
 btauto: $(BTAUTOVO) $(BTAUTOCMO)
+ltac: $(LTACVO) $(LTACCMO)
 
 .PHONY: omega micromega setoid_ring nsatz extraction
-.PHONY: fourier funind cc rtauto btauto
+.PHONY: fourier funind cc rtauto btauto ltac
 
 #################################
 ### Misc other development rules
-- 
cgit v1.2.3