17 files changed, 280 insertions, 0 deletions
diff --git a/.gitignore b/.gitignore
new file mode 100644
index 0000000..ce3c045
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1,3 @@
+doc
+html
+.pc
diff --git a/debian/changelog b/debian/changelog
new file mode 100644
index 0000000..abdad05
--- /dev/null
+++ b/debian/changelog
@@ -0,0 +1,128 @@
+aac-tactics (8.6-1) unstable; urgency=medium
+
+  * Team upload
+  * New upstream release
+  * Remove patch 001-fix-typos, applied upstream
+
+ -- Enrico Tassi <gareuselesinge@debian.org>  Tue, 27 Dec 2016 16:06:51 +0000
+
+aac-tactics (8.5.1-1) unstable; urgency=medium
+
+  * Team upload
+  * Imported Upstream version 8.5.1 (Closes: #813459)
+  * Use HTTPS for Vcs-* links
+  * New upstream URL & watch file
+  * Install .v files
+  * Fix installed docs
+  * Fix typos
+  * Bump Standards-Version to 3.9.8.
+    No change required
+
+ -- Nicolas Braud-Santoni <nicolas@braud-santoni.eu>  Sat, 23 Jul 2016 16:44:48 -0400
+
+aac-tactics (0.4-5) unstable; urgency=medium
+
+  * Recompile with OCaml 4.02.3
+
+ -- Stéphane Glondu <glondu@debian.org>  Wed, 14 Oct 2015 11:44:20 +0200
+
+aac-tactics (0.4-4) unstable; urgency=medium
+
+  * Fix Homepage URL
+  * Drop debian/watch
+  * Bump Standards-Version to 3.9.6
+  * Bump debhelper compat level to 9
+
+ -- Stéphane Glondu <glondu@debian.org>  Mon, 10 Aug 2015 21:16:02 +0200
+
+aac-tactics (0.4-3) unstable; urgency=medium
+
+  * Recompile with coq 8.4pl4
+
+ -- Stéphane Glondu <glondu@debian.org>  Wed, 30 Jul 2014 11:00:52 +0200
+
+aac-tactics (0.4-2) unstable; urgency=medium
+
+  * Recompile with coq 8.4pl3
+  * Bump Standards-Version to 3.9.5 (no changes)
+  * Update Vcs-*
+
+ -- Stéphane Glondu <glondu@debian.org>  Mon, 20 Jan 2014 08:22:59 +0100
+
+aac-tactics (0.4-1) unstable; urgency=low
+
+  * New upstream release
+
+ -- Stéphane Glondu <glondu@debian.org>  Thu, 05 Dec 2013 07:56:39 +0100
+
+aac-tactics (0.3.pl1-1) unstable; urgency=low
+
+  * New upstream release
+  * Use format version 1.0 in debian/copyright
+  * Bump Standards-Version to 3.9.4
+  * Upload to unstable
+
+ -- Stéphane Glondu <glondu@debian.org>  Thu, 09 May 2013 13:26:38 +0200
+
+aac-tactics (0.3-2) experimental; urgency=low
+
+  * Fix FTBFS without natdynlink
+  * This version requires the bugfix introduced in coq 8.4dfsg-2
+
+ -- Stéphane Glondu <glondu@debian.org>  Sat, 22 Sep 2012 16:08:20 +0200
+
+aac-tactics (0.3-1) experimental; urgency=low
+
+  * New upstream release
+
+ -- Stéphane Glondu <glondu@debian.org>  Fri, 21 Sep 2012 19:19:27 +0200
+
+aac-tactics (0.2.pl2-7) unstable; urgency=low
+
+  * Recompile with camlp5 6.06 (no changes)
+
+ -- Stéphane Glondu <glondu@debian.org>  Sat, 09 Jun 2012 10:31:21 +0200
+
+aac-tactics (0.2.pl2-6) unstable; urgency=medium
+
+  * Recompile with camlp5 6.05 and coq 8.3pl4 (no changes)
+
+ -- Stéphane Glondu <glondu@debian.org>  Sun, 01 Apr 2012 17:19:08 +0200
+
+aac-tactics (0.2.pl2-5) unstable; urgency=low
+
+  * Recompile with camlp5 6.04 (no changes)
+
+ -- Stéphane Glondu <glondu@debian.org>  Mon, 05 Mar 2012 21:51:05 +0100
+
+aac-tactics (0.2.pl2-4) unstable; urgency=low
+
+  * Rebuild with Coq 8.3pl3 (no source changes)
+
+ -- Stéphane Glondu <glondu@debian.org>  Sun, 25 Dec 2011 16:54:20 +0100
+
+aac-tactics (0.2.pl2-3) unstable; urgency=low
+
+  * Recompile with OCaml 3.12.1 (no changes)
+  * Bump Standards-Version to 3.9.2 (no changes)
+
+ -- Stéphane Glondu <glondu@debian.org>  Thu, 03 Nov 2011 06:41:57 +0100
+
+aac-tactics (0.2.pl2-2) unstable; urgency=low
+
+  * Upload to unstable
+
+ -- Stéphane Glondu <glondu@debian.org>  Sun, 01 May 2011 19:22:52 +0200
+
+aac-tactics (0.2.pl2-1) experimental; urgency=low
+
+  * New upstream release
+    - remove patch (applied upstream)
+
+ -- Stéphane Glondu <glondu@debian.org>  Mon, 28 Feb 2011 07:46:14 +0100
+
+aac-tactics (0.1-r13244-1) experimental; urgency=low
+
+  * Initial release (Closes: #605487)
+
+ -- Stéphane Glondu <glondu@debian.org>  Tue, 30 Nov 2010 16:24:53 +0100
diff --git a/debian/compat b/debian/compat
new file mode 100644
index 0000000..ec63514
--- /dev/null
+++ b/debian/compat
@@ -0,0 +1 @@
+9
diff --git a/debian/control b/debian/control
new file mode 100644
index 0000000..f4bf585
--- /dev/null
+++ b/debian/control
@@ -0,0 +1,59 @@
+Source: aac-tactics
+Section: math
+Priority: optional
+Maintainer: Debian OCaml Maintainers <debian-ocaml-maint@lists.debian.org>
+Uploaders: Stéphane Glondu <glondu@debian.org>
+Build-Depends:
+ debhelper (>= 9),
+ dh-ocaml (>= 0.9~),
+ ocaml-nox (>= 3.11.1-3~),
+ coq (>= 8.4dfsg-2~),
+ libcoq-ocaml-dev
+Standards-Version: 3.9.8
+Homepage: https://github.com/coq-contribs/aac-tactics
+Vcs-Browser: https://anonscm.debian.org/cgit/pkg-ocaml-maint/packages/aac-tactics.git
+Vcs-Git: https://anonscm.debian.org/git/pkg-ocaml-maint/packages/aac-tactics.git
+
+Package: libaac-tactics-ocaml
+Section: ocaml
+Architecture: any
+Depends:
+ ${ocaml:Depends},
+ ${shlibs:Depends},
+ ${misc:Depends}
+Recommends: libaac-tactics-coq
+Enhances: coq
+Provides: ${ocaml:Provides}
+Description: Coq tactics for reasoning modulo AC (plugin)
+ This Coq plugin provides tactics for rewriting universally quantified
+ equations, modulo associative (and possibly commutative) operators.
+ .
+ This package provides the plugin itself.
+
+Package: libaac-tactics-ocaml-dev
+Section: ocaml
+Architecture: any
+Depends:
+ ${ocaml:Depends},
+ ${shlibs:Depends},
+ ${misc:Depends}
+Provides: ${ocaml:Provides}
+Description: Coq tactics for reasoning modulo AC (devt files)
+ This Coq plugin provides tactics for rewriting universally quantified
+ equations, modulo associative (and possibly commutative) operators.
+ .
+ This package provides the static native-code library, needed to build
+ custom toplevels, and the compiled interfaces.
+
+Package: libaac-tactics-coq
+Architecture: all
+Depends:
+ libaac-tactics-ocaml (>= ${source:Version}),
+ coq-${F:CoqABI},
+ ${misc:Depends}
+Provides: aac-tactics
+Description: Coq tactics for reasoning modulo AC (theories)
+ This Coq plugin provides tactics for rewriting universally quantified
+ equations, modulo associative (and possibly commutative) operators.
+ .
+ This package provides the Coq support library.
diff --git a/debian/copyright b/debian/copyright
new file mode 100644
index 0000000..27e4338
--- /dev/null
+++ b/debian/copyright
@@ -0,0 +1,28 @@
+Format: http://www.debian.org/doc/packaging-manuals/copyright-format/1.0/
+Packaged-By: Stéphane Glondu <glondu@debian.org>
+Packaged-Date: Mon, 29 Nov 2010 23:40:57 +0100
+Source: http://sardes.inrialpes.fr/~braibant/aac_tactics/
+Upstream-Contact: Thomas Braibant, Damien Pous
+
+Files: *
+Copyright: 2009-2010, Thomas Braibant and Damien Pous
+License: LGPL-3+
+
+Files: debian/*
+Copyright: 2010, Stéphane Glondu <steph@glondu.net>
+License: LGPL-3+
+
+License: LGPL-3+
+ The aac_tactics plugin library is free software: you can
+ redistribute it and/or modify it under the terms of the GNU Lesser
+ General Public License as published by the Free Software Foundation,
+ either version 3 of the License, or (at your option) any later
+ version.
+ .
+ This library is distributed in the hope that it will be useful, but
+ WITHOUT ANY WARRANTY; without even the implied warranty of
+ MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
+ Lesser General Public License for more details.
+ .
+ On Debian systems, the complete text of the GNU Lesser General
+ Public License can be found in `/usr/share/common-licenses/LGPL-3'.
diff --git a/debian/gbp.conf b/debian/gbp.conf
new file mode 100644
index 0000000..cec628c
--- /dev/null
+++ b/debian/gbp.conf
@@ -0,0 +1,2 @@
+[DEFAULT]
+pristine-tar = True
diff --git a/debian/libaac-tactics-coq.doc-base.theories b/debian/libaac-tactics-coq.doc-base.theories
new file mode 100644
index 0000000..de3a8e5
--- /dev/null
+++ b/debian/libaac-tactics-coq.doc-base.theories
@@ -0,0 +1,8 @@
+Document: aac-tactics-theories
+Title: aac_tactics theories
+Abstract: Theories for aac_tactics (generated from .v sources via coqdoc)
+Section: Science/Mathematics
+
+Format: HTML
+Index: /usr/share/doc/libaac-tactics-coq/theories/index.html
+Files: /usr/share/doc/libaac-tactics-coq/theories/*
diff --git a/debian/libaac-tactics-coq.docs b/debian/libaac-tactics-coq.docs
new file mode 100644
index 0000000..e845566
--- /dev/null
+++ b/debian/libaac-tactics-coq.docs
@@ -0,0 +1 @@
+README
diff --git a/debian/libaac-tactics-coq.install b/debian/libaac-tactics-coq.install
new file mode 100644
index 0000000..b1c1948
--- /dev/null
+++ b/debian/libaac-tactics-coq.install
@@ -0,0 +1,3 @@
+                          /usr/lib/coq/user-contrib/AAC_tactics/*.v
+                          /usr/lib/coq/user-contrib/AAC_tactics/*.vo
+html/*                    /usr/share/doc/libaac-tactics-coq/theories
diff --git a/debian/libaac-tactics-ocaml-dev.install b/debian/libaac-tactics-ocaml-dev.install
new file mode 100644
index 0000000..18a9b3c
--- /dev/null
+++ b/debian/libaac-tactics-ocaml-dev.install
@@ -0,0 +1,2 @@
+         usr/lib/coq/user-contrib/AAC_tactics/*.cmi
+*.mli    usr/lib/coq/user-contrib/AAC_tactics/
diff --git a/debian/libaac-tactics-ocaml-dev.lintian-overrides b/debian/libaac-tactics-ocaml-dev.lintian-overrides
new file mode 100644
index 0000000..b102d8b
--- /dev/null
+++ b/debian/libaac-tactics-ocaml-dev.lintian-overrides
@@ -0,0 +1,2 @@
+# aac.cmo is a pack
+libaac-tactics-ocaml-dev: ocaml-dangling-cmi usr/lib/coq/user-contrib/AAC_tactics/aac.cmi
diff --git a/debian/libaac-tactics-ocaml-dev.ocamldoc b/debian/libaac-tactics-ocaml-dev.ocamldoc
new file mode 100644
index 0000000..f59e96e
--- /dev/null
+++ b/debian/libaac-tactics-ocaml-dev.ocamldoc
@@ -0,0 +1,3 @@
+-rectypes
+-I /usr/lib/coq/kernel -I /usr/lib/coq/proofs -I /usr/lib/coq/pretyping -I /usr/lib/coq/engine
+--include debian/libaac-tactics-ocaml-dev/usr/lib/coq
diff --git a/debian/libaac-tactics-ocaml.install.in b/debian/libaac-tactics-ocaml.install.in
new file mode 100644
index 0000000..b6795bd
--- /dev/null
+++ b/debian/libaac-tactics-ocaml.install.in
@@ -0,0 +1,2 @@
+     usr/lib/coq/user-contrib/AAC_tactics/*.cmo
+DYN: usr/lib/coq/user-contrib/AAC_tactics/*.cmxs
diff --git a/debian/rules b/debian/rules
new file mode 100755
index 0000000..e705617
--- /dev/null
+++ b/debian/rules
@@ -0,0 +1,32 @@
+#!/usr/bin/make -f
+# -*- makefile -*-
+
+include /usr/share/coq/coqvars.mk
+include /usr/share/ocaml/ocamlvars.mk
+
+ifeq ($(OCAML_NATDYNLINK),yes)
+  TARGET := opt
+else
+  TARGET := byte
+endif
+
+%:
+	dh $@ --with ocaml
+
+.PHONY: override_dh_auto_build
+override_dh_auto_build:
+	$(MAKE) Makefile.coq
+	$(MAKE) -f Makefile.coq $(TARGET) html
+
+.PHONY: override_dh_auto_install
+override_dh_auto_install:
+	$(MAKE) -f Makefile.coq install DSTROOT=$(CURDIR)/debian/tmp
+
+.PHONY: override_dh_install
+override_dh_install:
+	find debian/tmp -type f -name '*.glob' -delete
+	dh_install --fail-missing
+
+.PHONY: override_dh_gencontrol
+override_dh_gencontrol:
+	dh_gencontrol -- -VF:CoqABI="$(COQ_ABI)"
diff --git a/debian/source/format b/debian/source/format
new file mode 100644
index 0000000..163aaf8
--- /dev/null
+++ b/debian/source/format
@@ -0,0 +1 @@
+3.0 (quilt)
diff --git a/debian/source/local-options b/debian/source/local-options
new file mode 100644
index 0000000..c4cf480
--- /dev/null
+++ b/debian/source/local-options
@@ -0,0 +1,2 @@
+abort-on-upstream-changes
+unapply-patches
diff --git a/debian/watch b/debian/watch
new file mode 100644
index 0000000..11017f4
--- /dev/null
+++ b/debian/watch
@@ -0,0 +1,3 @@
+version=3
+opts=filenamemangle=s/.+\/v?(\d\S*)\.tar\.gz/aac-tactics-$1\.tar\.gz/ \
+  https://github.com/coq-contribs/aac-tactics/releases .*/v(\d+\.\d.\d)\.tar\.gz