From 155e671f7b83293ae327ddbd252d1d1ac961ab9a Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Mon, 9 Mar 2015 13:35:08 +0100
Subject: some work on ssreflect and discrete

---
 mathcomp/discrete/AUTHORS  |  1 +
 mathcomp/discrete/CeCILL-B |  1 +
 mathcomp/discrete/INSTALL  |  1 +
 mathcomp/discrete/Make     | 15 +++++++++++++++
 mathcomp/discrete/Makefile | 23 +++++++++++++++++++++++
 mathcomp/discrete/README   |  1 +
 mathcomp/discrete/all.v    | 15 ++++++++-------
 mathcomp/discrete/opam     | 12 ++++++++++++
 8 files changed, 62 insertions(+), 7 deletions(-)
 create mode 120000 mathcomp/discrete/AUTHORS
 create mode 120000 mathcomp/discrete/CeCILL-B
 create mode 120000 mathcomp/discrete/INSTALL
 create mode 100644 mathcomp/discrete/Make
 create mode 100644 mathcomp/discrete/Makefile
 create mode 120000 mathcomp/discrete/README
 create mode 100644 mathcomp/discrete/opam

(limited to 'mathcomp/discrete')

diff --git a/mathcomp/discrete/AUTHORS b/mathcomp/discrete/AUTHORS
new file mode 120000
index 0000000..b55a98d
--- /dev/null
+++ b/mathcomp/discrete/AUTHORS
@@ -0,0 +1 @@
+../../etc/AUTHORS
\ No newline at end of file
diff --git a/mathcomp/discrete/CeCILL-B b/mathcomp/discrete/CeCILL-B
new file mode 120000
index 0000000..83e22fd
--- /dev/null
+++ b/mathcomp/discrete/CeCILL-B
@@ -0,0 +1 @@
+../../etc/CeCILL-B
\ No newline at end of file
diff --git a/mathcomp/discrete/INSTALL b/mathcomp/discrete/INSTALL
new file mode 120000
index 0000000..6aa7ec5
--- /dev/null
+++ b/mathcomp/discrete/INSTALL
@@ -0,0 +1 @@
+../../etc/INSTALL
\ No newline at end of file
diff --git a/mathcomp/discrete/Make b/mathcomp/discrete/Make
new file mode 100644
index 0000000..bfbbfe2
--- /dev/null
+++ b/mathcomp/discrete/Make
@@ -0,0 +1,15 @@
+all.v
+bigop.v
+binomial.v
+choice.v
+div.v
+finfun.v
+fingraph.v
+finset.v
+fintype.v
+generic_quotient.v
+path.v
+prime.v
+tuple.v
+
+-R . mathcomp.discrete
diff --git a/mathcomp/discrete/Makefile b/mathcomp/discrete/Makefile
new file mode 100644
index 0000000..d693257
--- /dev/null
+++ b/mathcomp/discrete/Makefile
@@ -0,0 +1,23 @@
+H=@
+
+ifeq "$(COQBIN)" ""
+COQBIN=$(dir $(shell which coqtop))/
+endif
+
+
+OLD_MAKEFLAGS:=$(MAKEFLAGS)
+MAKEFLAGS+=-B
+
+.DEFAULT_GOAL := all
+
+%:
+	$(H)[ -e Makefile.coq ] || $(COQBIN)/coq_makefile -f Make -o Makefile.coq
+	$(H)MAKEFLAGS=$(OLD_MAKEFLAGS) $(MAKE) --no-print-directory \
+		-f Makefile.coq $*
+
+.PHONY: clean
+clean:
+	$(H)MAKEFLAGS=$(OLD_MAKEFLAGS) $(MAKE) --no-print-directory \
+		-f Makefile.coq clean
+	$(H)rm -f Makefile.coq
+
diff --git a/mathcomp/discrete/README b/mathcomp/discrete/README
new file mode 120000
index 0000000..e4e30e8
--- /dev/null
+++ b/mathcomp/discrete/README
@@ -0,0 +1 @@
+../../etc/README
\ No newline at end of file
diff --git a/mathcomp/discrete/all.v b/mathcomp/discrete/all.v
index d100add..8412bdb 100644
--- a/mathcomp/discrete/all.v
+++ b/mathcomp/discrete/all.v
@@ -1,12 +1,13 @@
-Require Export bigop.
-Require Export binomial.
+Require Export mathcomp.ssreflect.all.
 Require Export choice.
+Require Export path.
 Require Export div.
-Require Export finfun.
+Require Export fintype.
 Require Export fingraph.
+Require Export tuple.
+Require Export finfun.
+Require Export bigop.
+Require Export prime.
 Require Export finset.
-Require Export fintype.
+Require Export binomial.
 Require Export generic_quotient.
-Require Export path.
-Require Export prime.
-Require Export tuple.
diff --git a/mathcomp/discrete/opam b/mathcomp/discrete/opam
new file mode 100644
index 0000000..3646845
--- /dev/null
+++ b/mathcomp/discrete/opam
@@ -0,0 +1,12 @@
+opam-version: "1.2"
+name: "coq:mathcomp:discrete"
+version: "1.5"
+maintainer: "Ssreflect <ssreflect@msr-inria.inria.fr>"
+authors: "Ssreflect <ssreflect@msr-inria.inria.fr>"
+homepage: "http://ssr.msr-inria.inria.fr/"
+bug-reports: "ssreflect@msr-inria.inria.fr"
+license: "CeCILL-B"
+build: [ make "-j" "%{jobs}%" ] 
+install: [ make "install" ]
+remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/mathcomp/discrete'" ]
+depends: [ "coq:mathcomp:ssreflect" { = "1.5" } ]
-- 
cgit v1.2.3