adding "Make" and "Makefile"

.gitignore

@@ -1,5 +1,3 @@
-Make
-Makefile
 Makefile.bak
 *.v.d
 *.vo

Make

@@ -0,0 +1,132 @@
+# Library name
+-R . MathClasses
+
+# Coq files (filled by the configure)
+./misc/util.v
+./misc/setoid_tactics.v
+./misc/decision.v
+./misc/JMrelation.v
+./misc/stdlib_hints.v
+./misc/workarounds.v
+./misc/propholds.v
+./misc/workaround_tactics.v
+./functors/constant.v
+./varieties/abgroup.v
+./varieties/monoids.v
+./varieties/setoids.v
+./varieties/groups.v
+./varieties/open_terms.v
+./varieties/closed_terms.v
+./varieties/semigroups.v
+./varieties/empty.v
+./varieties/rings.v
+./varieties/semirings.v
+./categories/product.v
+./categories/categories.v
+./categories/varieties.v
+./categories/dual.v
+./categories/setoids.v
+./categories/JMcat.v
+./categories/unit.v
+./categories/orders.v
+./categories/algebras.v
+./categories/empty.v
+./categories/functors.v
+./quote/classquote.v
+./implementations/ZType_integers.v
+./implementations/stdlib_binary_integers.v
+./implementations/stdlib_binary_naturals.v
+./implementations/bool.v
+./implementations/mset_finite_set.v
+./implementations/intfrac_rationals.v
+./implementations/fast_naturals.v
+./implementations/option.v
+./implementations/stdlib_rationals.v
+./implementations/fast_rationals.v
+./implementations/list.v
+./implementations/modular_ring.v
+./implementations/list_finite_set.v
+./implementations/NType_naturals.v
+./implementations/positive_semiring_elements.v
+./implementations/polynomials.v
+./implementations/nonzero_field_elements.v
+./implementations/field_of_fractions.v
+./implementations/ne_list.v
+./implementations/nonneg_integers_naturals.v
+./implementations/natpair_integers.v
+./implementations/peano_naturals.v
+./implementations/semiring_pairs.v
+./implementations/nonneg_semiring_elements.v
+./implementations/fast_integers.v
+./implementations/dyadics.v
+./implementations/QType_rationals.v
+./interfaces/abstract_algebra.v
+./interfaces/vectorspace.v
+./interfaces/naturals.v
+./interfaces/finite_sets.v
+./interfaces/universal_algebra.v
+./interfaces/additional_operations.v
+./interfaces/rationals.v
+./interfaces/canonical_names.v
+./interfaces/orders.v
+./interfaces/monads.v
+./interfaces/sequences.v
+./interfaces/ua_basic.v
+./interfaces/integers.v
+./interfaces/functors.v
+./orders/naturals.v
+./orders/minmax.v
+./orders/maps.v
+./orders/dec_fields.v
+./orders/rationals.v
+./orders/orders.v
+./orders/nat_int.v
+./orders/rings.v
+./orders/integers.v
+./orders/lattices.v
+./orders/semirings.v
+./theory/quote_monoid.v
+./theory/naturals.v
+./theory/categories.v
+./theory/ua_packed.v
+./theory/nat_distance.v
+./theory/setoids.v
+./theory/products.v
+./theory/groups.v
+./theory/finite_sets.v
+./theory/abs.v
+./theory/ua_subalgebraT.v
+./theory/strong_setoids.v
+./theory/monoid_normalization.v
+./theory/series.v
+./theory/dec_fields.v
+./theory/ua_mapped_operations.v
+./theory/ua_term_monad.v
+./theory/fields.v
+./theory/ua_homomorphisms.v
+./theory/rationals.v
+./theory/ua_subalgebra.v
+./theory/ua_transference.v
+./theory/streams.v
+./theory/ring_ideals.v
+./theory/monads.v
+./theory/ring_congruence.v
+./theory/hom_functor.v
+./theory/sequences.v
+./theory/forget_variety.v
+./theory/ua_congruence.v
+./theory/rings.v
+./theory/int_abs.v
+./theory/int_to_nat.v
+./theory/adjunctions.v
+./theory/nat_pow.v
+./theory/integers.v
+./theory/lattices.v
+./theory/jections.v
+./theory/cut_minus.v
+./theory/ua_subvariety.v
+./theory/int_pow.v
+./theory/ua_products.v
+./theory/forget_algebra.v
+./theory/shiftl.v
+./theory/functors.v

Makefile

@@ -0,0 +1,14 @@
+all: Makefile.coq
+	+make -f Makefile.coq all
+
+clean: Makefile.coq
+	+make -f Makefile.coq clean
+	rm -f Makefile.coq
+
+Makefile.coq: Make
+	$(COQBIN)coq_makefile -f Make -o Makefile.coq
+
+%: Makefile.coq
+	+make -f Makefile.coq $@
+
+.PHONY: all clean