character packaged

math-comp · Mar 30, 2015 · 086f066 · 086f066
1 parent 821071c
commit 086f066
Show file tree

Hide file tree

Showing 7 changed files with 50 additions and 0 deletions.
diff --git a/mathcomp/character/AUTHORS b/mathcomp/character/AUTHORS
@@ -0,0 +1 @@
+../../etc/AUTHORS
diff --git a/mathcomp/character/CeCILL-B b/mathcomp/character/CeCILL-B
@@ -0,0 +1 @@
+../../etc/CeCILL-B
diff --git a/mathcomp/character/INSTALL b/mathcomp/character/INSTALL
@@ -0,0 +1 @@
+../../etc/INSTALL
diff --git a/mathcomp/character/Make b/mathcomp/character/Make
@@ -0,0 +1,11 @@
+all.v
+character.v
+classfun.v
+finfield.v
+inertia.v
+integral_char.v
+mxabelem.v
+mxrepresentation.v
+vcharacter.v
+
+-R . mathcomp.character
diff --git a/mathcomp/character/Makefile b/mathcomp/character/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/character/README b/mathcomp/character/README
@@ -0,0 +1 @@
+../../etc/README
diff --git a/mathcomp/character/opam b/mathcomp/character/opam
@@ -0,0 +1,12 @@
+opam-version: "1.2"
+name: "coq:mathcomp:character"
+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/character'" ]
+depends: [ "coq:mathcomp:field" { = "1.5" } ]