aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2017-10-27 19:26:31 +0200
committerPierre-Marie Pédrot2017-10-27 19:32:11 +0200
commit216c5f25cf41d68871149f21f83518ec0a4f1cc9 (patch)
tree07ce377c770c700c904205a1fcab08d2f1f142fa
parenta7c83429db05866dfc9613fc4a488d62d31386fc (diff)
Adding an OPAM package.
-rw-r--r--Makefile16
-rw-r--r--opam/descr1
-rw-r--r--opam/opam17
3 files changed, 25 insertions, 9 deletions
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
diff --git a/opam/descr b/opam/descr
new file mode 100644
index 0000000000..82463c4f45
--- /dev/null
+++ b/opam/descr
@@ -0,0 +1 @@
+A tactic language for Coq.
diff --git a/opam/opam b/opam/opam
new file mode 100644
index 0000000000..e461b97942
--- /dev/null
+++ b/opam/opam
@@ -0,0 +1,17 @@
+opam-version: "1.2"
+name: "coq-ltac2"
+version: "0.1"
+maintainer: "Pierre-Marie Pédrot <pierre-marie.pedrot@irif.fr>"
+author: "Pierre-Marie Pédrot <pierre-marie.pedrot@irif.fr>"
+license: "LGPL 2.1"
+homepage: "https://github.com/ppedrot/ltac2"
+dev-repo: "https://github.com/ppedrot/ltac2.git"
+bug-reports: "https://github.com/ppedrot/ltac2/issues"
+build: [
+ [make "COQBIN=\"\"" "-j%{jobs}%"]
+]
+install: [make "install"]
+remove: [make "uninstall"]
+depends: [
+ "coq" { = "dev" }
+]