From c25e86e6b4e8bb694d3c8e50f04a92cc33ad807d Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 24 Jul 2017 17:41:01 +0200
Subject: Turning the ltac2 subfolder into a standalone plugin.

---
 Makefile | 12 ++++++++++++
 1 file changed, 12 insertions(+)
 create mode 100644 Makefile

(limited to 'Makefile')

diff --git a/Makefile b/Makefile
new file mode 100644
index 0000000000..cfdeeba747
--- /dev/null
+++ b/Makefile
@@ -0,0 +1,12 @@
+all: Makefile.coq
+	$(MAKE) -f Makefile.coq
+
+install: all
+	$(MAKE) -f Makefile.coq install
+
+clean: Makefile.coq
+	$(MAKE) -f Makefile.coq clean
+	rm -f Makefile.coq
+
+Makefile.coq: _CoqProject
+	$(COQBIN)/coq_makefile -f _CoqProject -o Makefile.coq
-- 
cgit v1.2.3


From 2a74da7b6f275634fd8ed9c209edc73f2ae15427 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 26 Jul 2017 16:38:52 +0200
Subject: Adding a file for testing typing.

---
 Makefile | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'Makefile')

diff --git a/Makefile b/Makefile
index cfdeeba747..d555fea236 100644
--- a/Makefile
+++ b/Makefile
@@ -10,3 +10,7 @@ clean: Makefile.coq
 
 Makefile.coq: _CoqProject
 	$(COQBIN)/coq_makefile -f _CoqProject -o Makefile.coq
+
+tests: all
+	@$(MAKE) -C tests -s clean
+	@$(MAKE) -C tests -s all
-- 
cgit v1.2.3


From 216c5f25cf41d68871149f21f83518ec0a4f1cc9 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 27 Oct 2017 19:26:31 +0200
Subject: Adding an OPAM package.

---
 Makefile | 16 +++++++---------
 1 file changed, 7 insertions(+), 9 deletions(-)

(limited to 'Makefile')

diff --git a/Makefile b/Makefile
index d555fea236..e0e197650d 100644
--- a/Makefile
+++ b/Makefile
@@ -1,16 +1,14 @@
-all: Makefile.coq
-	$(MAKE) -f Makefile.coq
+ifeq "$(COQBIN)" ""
+  COQBIN=$(dir $(shell which coqtop))/
+endif
 
-install: all
-	$(MAKE) -f Makefile.coq install
-
-clean: Makefile.coq
-	$(MAKE) -f Makefile.coq clean
-	rm -f Makefile.coq
+%: Makefile.coq
 
 Makefile.coq: _CoqProject
-	$(COQBIN)/coq_makefile -f _CoqProject -o Makefile.coq
+	$(COQBIN)coq_makefile -f _CoqProject -o Makefile.coq
 
 tests: all
 	@$(MAKE) -C tests -s clean
 	@$(MAKE) -C tests -s all
+
+-include Makefile.coq
-- 
cgit v1.2.3


From 66b6e83f4f4c32ad86333e13d65329be02c46048 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 25 Apr 2019 12:02:43 +0200
Subject: Prepare merge into Coq

---
 Makefile | 14 --------------
 1 file changed, 14 deletions(-)
 delete mode 100644 Makefile

(limited to 'Makefile')

diff --git a/Makefile b/Makefile
deleted file mode 100644
index e0e197650d..0000000000
--- a/Makefile
+++ /dev/null
@@ -1,14 +0,0 @@
-ifeq "$(COQBIN)" ""
-  COQBIN=$(dir $(shell which coqtop))/
-endif
-
-%: Makefile.coq
-
-Makefile.coq: _CoqProject
-	$(COQBIN)coq_makefile -f _CoqProject -o Makefile.coq
-
-tests: all
-	@$(MAKE) -C tests -s clean
-	@$(MAKE) -C tests -s all
-
--include Makefile.coq
-- 
cgit v1.2.3


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 | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'Makefile')

diff --git a/Makefile b/Makefile
index 2b5d2cea16..c4404d13c7 100644
--- a/Makefile
+++ b/Makefile
@@ -66,7 +66,7 @@ FIND_SKIP_DIRS:='(' \
 ')' -prune -o
 
 define find
- $(shell find . $(FIND_SKIP_DIRS) '(' -name $(1) ')' -print | sed 's|^\./||')
+ $(shell find . user-contrib/Ltac2 $(FIND_SKIP_DIRS) '(' -name $(1) ')' -print | sed 's|^\./||')
 endef
 
 define findindir
-- 
cgit v1.2.3