remove checker/Makefile

 This historical Makefile was used during the development of coqcheck,
 but was unused since then : the checker is built via Coq's main Makefile.
 So let's remove this one to avoid any risk of confusion.

1 files changed, 0 insertions, 88 deletions

diff --git a/checker/Makefile b/checker/Makefile
deleted file mode 100644
index 2bcc9d3656..0000000000
--- a/checker/Makefile
+++ /dev/null
@@ -1,88 +0,0 @@
-OCAMLC=ocamlc
-OCAMLOPT=ocamlopt
-
-COQSRC=..
-
-MLDIRS=-I $(COQSRC)/config -I $(COQSRC)/lib -I $(COQSRC)/kernel -I +camlp4
-BYTEFLAGS=$(MLDIRS)
-OPTFLAGS=$(MLDIRS)
-
-CHECKERNAME=coqchk
-
-BINARIES=../bin/$(CHECKERNAME)$(EXE) ../bin/$(CHECKERNAME).opt$(EXE)
-MCHECKERLOCAL :=\
-  declarations.cmo environ.cmo \
-  closure.cmo reduction.cmo \
-  type_errors.cmo \
-  modops.cmo \
-  inductive.cmo typeops.cmo \
-  indtypes.cmo subtyping.cmo mod_checking.cmo \
-validate.cmo \
-  safe_typing.cmo check.cmo \
-  check_stat.cmo checker.cmo
-
-MCHECKER:=\
-  $(COQSRC)/config/coq_config.cmo \
-  $(COQSRC)/lib/pp_control.cmo $(COQSRC)/lib/pp.cmo $(COQSRC)/lib/compat.cmo \
-  $(COQSRC)/lib/util.cmo $(COQSRC)/lib/option.cmo $(COQSRC)/lib/hashcons.cmo \
-  $(COQSRC)/lib/system.cmo $(COQSRC)/lib/flags.cmo \
-  $(COQSRC)/lib/predicate.cmo $(COQSRC)/lib/rtree.cmo \
-  $(COQSRC)/kernel/names.cmo $(COQSRC)/kernel/univ.cmo \
-  $(COQSRC)/kernel/esubst.cmo term.cmo \
-  $(MCHECKERLOCAL)
-
-all: $(BINARIES)
-
-byte : ../bin/$(CHECKERNAME)$(EXE)
-opt : ../bin/$(CHECKERNAME).opt$(EXE)
-
-check.cma: $(MCHECKERLOCAL)
-	ocamlc $(BYTEFLAGS) -a -o $@ $(MCHECKER)
-
-check.cmxa: $(MCHECKERLOCAL:.cmo=.cmx)
-	ocamlopt $(OPTFLAGS) -a -o $@ $(MCHECKER:.cmo=.cmx)
-
-../bin/$(CHECKERNAME)$(EXE): check.cma
-	ocamlc $(BYTEFLAGS) -o $@ unix.cma gramlib.cma check.cma main.ml
-
-../bin/$(CHECKERNAME).opt$(EXE): check.cmxa
-	ocamlopt $(OPTFLAGS) -o $@ unix.cmxa gramlib.cmxa check.cmxa main.ml
-
-stats:
-	@echo STRUCTURE
-	@wc names.ml term.ml declarations.ml environ.ml type_errors.ml
-	@echo
-	@echo REDUCTION
-	@-wc esubst.ml closure.ml reduction.ml
-	@echo
-	@echo TYPAGE
-	@wc univ.ml inductive.ml indtypes.ml typeops.ml safe_typing.ml
-	@echo
-	@echo MODULES
-	@wc modops.ml subtyping.ml
-	@echo
-	@echo INTERFACE
-	@wc check*.ml main.ml 
-	@echo
-	@echo TOTAL
-	@wc *.ml | tail -1
-
-.SUFFIXES:.ml .mli .cmi .cmo .cmx
-
-.ml.cmo:
-	$(OCAMLC) -c $(BYTEFLAGS) $<
-
-.ml.cmx:
-	$(OCAMLOPT) -c $(OPTFLAGS) $<
-
-.mli.cmi:
-	$(OCAMLC) -c $(BYTEFLAGS) $<
-
-
-depend::
-	ocamldep *.ml* > .depend
-
-clean::
-	rm -f *.cm* *.o *.a *~ $(BINARIES)
-
--include .depend