aboutsummaryrefslogtreecommitdiff
path: root/mathcomp
diff options
context:
space:
mode:
Diffstat (limited to 'mathcomp')
l---------mathcomp/discrete/AUTHORS1
l---------mathcomp/discrete/CeCILL-B1
l---------mathcomp/discrete/INSTALL1
-rw-r--r--mathcomp/discrete/Make15
-rw-r--r--mathcomp/discrete/Makefile23
l---------mathcomp/discrete/README1
-rw-r--r--mathcomp/discrete/all.v15
-rw-r--r--mathcomp/discrete/opam12
l---------mathcomp/ssreflect/AUTHORS1
l---------mathcomp/ssreflect/CeCILL-B1
l---------mathcomp/ssreflect/INSTALL1
-rw-r--r--mathcomp/ssreflect/Make8
-rw-r--r--mathcomp/ssreflect/Makefile33
l---------mathcomp/ssreflect/README1
-rw-r--r--mathcomp/ssreflect/all.v7
-rw-r--r--mathcomp/ssreflect/opam12
16 files changed, 110 insertions, 23 deletions
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" } ]
diff --git a/mathcomp/ssreflect/AUTHORS b/mathcomp/ssreflect/AUTHORS
new file mode 120000
index 0000000..b55a98d
--- /dev/null
+++ b/mathcomp/ssreflect/AUTHORS
@@ -0,0 +1 @@
+../../etc/AUTHORS \ No newline at end of file
diff --git a/mathcomp/ssreflect/CeCILL-B b/mathcomp/ssreflect/CeCILL-B
new file mode 120000
index 0000000..83e22fd
--- /dev/null
+++ b/mathcomp/ssreflect/CeCILL-B
@@ -0,0 +1 @@
+../../etc/CeCILL-B \ No newline at end of file
diff --git a/mathcomp/ssreflect/INSTALL b/mathcomp/ssreflect/INSTALL
new file mode 120000
index 0000000..6aa7ec5
--- /dev/null
+++ b/mathcomp/ssreflect/INSTALL
@@ -0,0 +1 @@
+../../etc/INSTALL \ No newline at end of file
diff --git a/mathcomp/ssreflect/Make b/mathcomp/ssreflect/Make
index 9e7c5db..6c76897 100644
--- a/mathcomp/ssreflect/Make
+++ b/mathcomp/ssreflect/Make
@@ -6,3 +6,11 @@ ssreflect.v
ssrfun.v
ssrmatching.v
ssrnat.v
+
+ssreflect.mllib
+ssrmatching.mli
+ssrmatching.ml4
+ssreflect.ml4
+
+-I .
+-R . mathcomp.ssreflect
diff --git a/mathcomp/ssreflect/Makefile b/mathcomp/ssreflect/Makefile
index 46a2d69..12c71fc 100644
--- a/mathcomp/ssreflect/Makefile
+++ b/mathcomp/ssreflect/Makefile
@@ -1,3 +1,5 @@
+H=@
+
ifeq "$(COQBIN)" ""
COQBIN=$(dir $(shell which coqtop))/
endif
@@ -13,21 +15,28 @@ endif
OLD_MAKEFLAGS:=$(MAKEFLAGS)
MAKEFLAGS+=-B
+.DEFAULT_GOAL := all
+
%:
- @[ -e Makefile.coq ] || $(call coqmakefile)
- @[ Make -ot Makefile.coq ] || $(call coqmakefile)
- @MAKEFLAGS=$(OLD_MAKEFLAGS) $(MAKE) --no-print-directory \
- -f Makefile.coq $*
+ $(H)[ -e Makefile.coq ] || $(call coqmakefile)
+# Override COQLIBS to find the "right" copy .ml files, otherwise
+# coq_makefile uses only the -R in COQLIBS and ignores the -I in
+# OCAMLLIBS to look for .ml files in order to generate .d files
+# via coqdep
+ $(H)MAKEFLAGS=$(OLD_MAKEFLAGS) $(MAKE) --no-print-directory \
+ -f Makefile.coq $* \
+ COQLIBS='-I . -R . mathcomp.ssreflect'
define coqmakefile
(echo "Generating Makefile.coq for Coq $(V) with COQBIN=$(COQBIN)";\
- cp Make Make.coq;\
- echo -I plugin/$(V)/src >> Make.coq;\
- echo plugin/$(V)/src/ssreflect.mllib >> Make.coq;\
- echo plugin/$(V)/src/ssrmatching.mli >> Make.coq;\
- echo plugin/$(V)/src/ssrmatching.ml4 >> Make.coq;\
- echo plugin/$(V)/src/ssreflect.ml4 >> Make.coq;\
- $(COQBIN)/coq_makefile -f Make.coq -o Makefile.coq)
+ ln -sf plugin/$(V)/ssreflect.mllib .;\
+ ln -sf plugin/$(V)/ssrmatching.mli .;\
+ ln -sf plugin/$(V)/ssrmatching.ml4 .;\
+ ln -sf plugin/$(V)/ssreflect.ml4 .;\
+ $(COQBIN)/coq_makefile -f Make -o Makefile.coq)
endef
-
+clean:
+ $(H)MAKEFLAGS=$(OLD_MAKEFLAGS) $(MAKE) --no-print-directory \
+ -f Makefile.coq clean
+ $(H)rm -f Makefile.coq
diff --git a/mathcomp/ssreflect/README b/mathcomp/ssreflect/README
new file mode 120000
index 0000000..e4e30e8
--- /dev/null
+++ b/mathcomp/ssreflect/README
@@ -0,0 +1 @@
+../../etc/README \ No newline at end of file
diff --git a/mathcomp/ssreflect/all.v b/mathcomp/ssreflect/all.v
index c441810..ce3e470 100644
--- a/mathcomp/ssreflect/all.v
+++ b/mathcomp/ssreflect/all.v
@@ -1,7 +1,6 @@
-Require Export eqtype.
-Require Export seq.
-Require Export ssrbool.
Require Export ssreflect.
+Require Export ssrbool.
Require Export ssrfun.
-Require Export ssrmatching.
+Require Export eqtype.
Require Export ssrnat.
+Require Export seq.
diff --git a/mathcomp/ssreflect/opam b/mathcomp/ssreflect/opam
new file mode 100644
index 0000000..bef7ebd
--- /dev/null
+++ b/mathcomp/ssreflect/opam
@@ -0,0 +1,12 @@
+opam-version: "1.2"
+name: "coq:mathcomp:ssreflect"
+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/ssreflect'" ]
+depends: [ "coq" { ( >= "8.4pl4" & < "8.5" ) | ( = "8.5beta1" ) } ]
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 19:16:13 +0000