Répertoire Numbers poursuit l'objectif entamé en syntaxe V7 dans le

répertoire Num. Suppression de ce dernier de l'archive courante.



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9995 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 0 insertions, 343 deletions

diff --git a/theories/Num/Makefile b/theories/Num/Makefile
deleted file mode 100644
index fdbe44bb6d..0000000000
--- a/theories/Num/Makefile
+++ /dev/null
@@ -1,343 +0,0 @@
-##############################################################################
-##                 The Calculus of Inductive Constructions                  ##
-##                                                                          ##
-##                                Projet Coq                                ##
-##                                                                          ##
-##                     INRIA                        ENS-CNRS                ##
-##              Rocquencourt                        Lyon                    ##
-##                                                                          ##
-##                                  Coq V7                                  ##
-##                                                                          ##
-##                                                                          ##
-##############################################################################
-
-# WARNING
-#
-# This Makefile has been automagically generated by coq_makefile
-# Edit at your own risks !
-#
-# END OF WARNING
-
-#
-# This Makefile was generated by the command line :
-# coq_makefile -f Make -o Makefile 
-#
-
-##########################
-#                        #
-# Variables definitions. #
-#                        #
-##########################
-
-CAMLP4LIB=`camlp4 -where`
-COQSRC=-I $(COQTOP)/kernel -I $(COQTOP)/lib \
-  -I $(COQTOP)/library -I $(COQTOP)/parsing -I $(COQTOP)/pretyping \
-  -I $(COQTOP)/proofs -I $(COQTOP)/syntax -I $(COQTOP)/tactics \
-  -I $(COQTOP)/toplevel -I $(CAMLP4LIB)
-ZFLAGS=$(OCAMLLIBS) $(COQSRC)
-OPT=
-COQFLAGS=-q $(OPT) $(COQLIBS)
-COQC=$(COQBIN)coqc
-GALLINA=gallina
-COQ2HTML=coq2html
-COQ2LATEX=coq2latex
-CAMLC=ocamlc -c
-CAMLOPTC=ocamlopt -c
-CAMLLINK=ocamlc
-CAMLOPTLINK=ocamlopt
-COQDEP=$(COQBIN)coqdep -c
-COQVO2XML=coq_vo2xml
-
-#########################
-#                       #
-# Libraries definition. #
-#                       #
-#########################
-
-OCAMLLIBS=-I .
-COQLIBS=-I .
-
-###################################
-#                                 #
-# Definition of the "all" target. #
-#                                 #
-###################################
-
-all: Params.vo\
-  EqParams.vo\
-  NSyntax.vo\
-  Axioms.vo\
-  EqAxioms.vo\
-  NeqParams.vo\
-  NeqAxioms.vo\
-  NeqDef.vo\
-  NeqProps.vo\
-  AddProps.vo\
-  LtProps.vo\
-  OppProps.vo\
-  SubProps.vo\
-  LeAxioms.vo\
-  LeProps.vo\
-  GtAxioms.vo\
-  GtProps.vo\
-  GeAxioms.vo\
-  GeProps.vo\
-  DiscrAxioms.vo\
-  DiscrProps.vo\
-  OppAxioms.vo\
-  Leibniz\
-  Nat
-
-spec: Params.vi\
-  EqParams.vi\
-  NSyntax.vi\
-  Axioms.vi\
-  EqAxioms.vi\
-  NeqParams.vi\
-  NeqAxioms.vi\
-  NeqDef.vi\
-  NeqProps.vi\
-  AddProps.vi\
-  LtProps.vi\
-  OppProps.vi\
-  SubProps.vi\
-  LeAxioms.vi\
-  LeProps.vi\
-  GtAxioms.vi\
-  GtProps.vi\
-  GeAxioms.vi\
-  GeProps.vi\
-  DiscrAxioms.vi\
-  DiscrProps.vi\
-  OppAxioms.vi
-
-gallina: Params.g\
-  EqParams.g\
-  NSyntax.g\
-  Axioms.g\
-  EqAxioms.g\
-  NeqParams.g\
-  NeqAxioms.g\
-  NeqDef.g\
-  NeqProps.g\
-  AddProps.g\
-  LtProps.g\
-  OppProps.g\
-  SubProps.g\
-  LeAxioms.g\
-  LeProps.g\
-  GtAxioms.g\
-  GtProps.g\
-  GeAxioms.g\
-  GeProps.g\
-  DiscrAxioms.g\
-  DiscrProps.g\
-  OppAxioms.g
-
-html: Params.html\
-  EqParams.html\
-  NSyntax.html\
-  Axioms.html\
-  EqAxioms.html\
-  NeqParams.html\
-  NeqAxioms.html\
-  NeqDef.html\
-  NeqProps.html\
-  AddProps.html\
-  LtProps.html\
-  OppProps.html\
-  SubProps.html\
-  LeAxioms.html\
-  LeProps.html\
-  GtAxioms.html\
-  GtProps.html\
-  GeAxioms.html\
-  GeProps.html\
-  DiscrAxioms.html\
-  DiscrProps.html\
-  OppAxioms.html
-
-tex: Params.tex\
-  EqParams.tex\
-  NSyntax.tex\
-  Axioms.tex\
-  EqAxioms.tex\
-  NeqParams.tex\
-  NeqAxioms.tex\
-  NeqDef.tex\
-  NeqProps.tex\
-  AddProps.tex\
-  LtProps.tex\
-  OppProps.tex\
-  SubProps.tex\
-  LeAxioms.tex\
-  LeProps.tex\
-  GtAxioms.tex\
-  GtProps.tex\
-  GeAxioms.tex\
-  GeProps.tex\
-  DiscrAxioms.tex\
-  DiscrProps.tex\
-  OppAxioms.tex
-
-gallinatex: Params.g.tex\
-  EqParams.g.tex\
-  NSyntax.g.tex\
-  Axioms.g.tex\
-  EqAxioms.g.tex\
-  NeqParams.g.tex\
-  NeqAxioms.g.tex\
-  NeqDef.g.tex\
-  NeqProps.g.tex\
-  AddProps.g.tex\
-  LtProps.g.tex\
-  OppProps.g.tex\
-  SubProps.g.tex\
-  LeAxioms.g.tex\
-  LeProps.g.tex\
-  GtAxioms.g.tex\
-  GtProps.g.tex\
-  GeAxioms.g.tex\
-  GeProps.g.tex\
-  DiscrAxioms.g.tex\
-  DiscrProps.g.tex\
-  OppAxioms.g.tex
-
-gallinahtml: Params.g.html\
-  EqParams.g.html\
-  NSyntax.g.html\
-  Axioms.g.html\
-  EqAxioms.g.html\
-  NeqParams.g.html\
-  NeqAxioms.g.html\
-  NeqDef.g.html\
-  NeqProps.g.html\
-  AddProps.g.html\
-  LtProps.g.html\
-  OppProps.g.html\
-  SubProps.g.html\
-  LeAxioms.g.html\
-  LeProps.g.html\
-  GtAxioms.g.html\
-  GtProps.g.html\
-  GeAxioms.g.html\
-  GeProps.g.html\
-  DiscrAxioms.g.html\
-  DiscrProps.g.html\
-  OppAxioms.g.html
-
-xml:: .xml_time_stamp
-.xml_time_stamp: Params.vo\
-  EqParams.vo\
-  NSyntax.vo\
-  Axioms.vo\
-  EqAxioms.vo\
-  NeqParams.vo\
-  NeqAxioms.vo\
-  NeqDef.vo\
-  NeqProps.vo\
-  AddProps.vo\
-  LtProps.vo\
-  OppProps.vo\
-  SubProps.vo\
-  LeAxioms.vo\
-  LeProps.vo\
-  GtAxioms.vo\
-  GtProps.vo\
-  GeAxioms.vo\
-  GeProps.vo\
-  DiscrAxioms.vo\
-  DiscrProps.vo\
-  OppAxioms.vo
-	$(COQVO2XML) $(COQFLAGS) $(?:%.o=%)
-	touch .xml_time_stamp
-
-###################
-#                 #
-# Subdirectories. #
-#                 #
-###################
-
-Leibniz:
-	cd Leibniz ; $(MAKE) all
-
-Nat:
-	cd Nat ; $(MAKE) all
-
-####################
-#                  #
-# Special targets. #
-#                  #
-####################
-
-.PHONY: all opt byte archclean clean install depend xml Leibniz Nat
-
-.SUFFIXES: .v .vo .vi .g .html .tex .g.tex .g.html
-
-.v.vo:
-	$(COQC) $(COQDEBUG) $(COQFLAGS) $*
-
-.v.vi:
-	$(COQC) -i $(COQDEBUG) $(COQFLAGS) $*
-
-.v.g:
-	$(GALLINA) $<
-
-.v.html:
-	$(COQ2HTML) $<
-
-.v.tex:
-	$(COQ2LATEX) $< -latex -o $@
-
-.v.g.html:
-	$(GALLINA) -stdout $< | $(COQ2HTML) -f > $@
-
-.v.g.tex:
-	$(GALLINA) -stdout $< | $(COQ2LATEX) - -latex -o $@
-
-byte:
-	$(MAKE) all "OPT="
-
-opt:
-	$(MAKE) all "OPT=-opt"
-
-include .depend
-
-depend:
-	rm .depend
-	$(COQDEP) -i $(COQLIBS) *.v *.ml *.mli >.depend
-	$(COQDEP) $(COQLIBS) -suffix .html *.v >>.depend
-	(cd Leibniz ; $(MAKE) depend)
-	(cd Nat ; $(MAKE) depend)
-
-xml::
-	(cd Leibniz ; $(MAKE) xml)
-	(cd Nat ; $(MAKE) xml)
-
-install:
-	@if test -z $(TARGETDIR); then echo "You must set TARGETDIR (for instance with 'make TARGETDIR=foobla install')"; exit 1; fi
-	cp -f *.vo $(TARGETDIR)
-	(cd Leibniz ; $(MAKE) install)
-	(cd Nat ; $(MAKE) install)
-
-Makefile: Make
-	mv -f Makefile Makefile.bak
-	$(COQBIN)coq_makefile -f Make -o Makefile
-
-clean:
-	rm -f *.cmo *.cmi *.cmx *.o *.vo *.vi *~
-	(cd Leibniz ; $(MAKE) clean)
-	(cd Nat ; $(MAKE) clean)
-
-archclean:
-	rm -f *.cmx *.o
-	(cd Leibniz ; $(MAKE) archclean)
-	(cd Nat ; $(MAKE) archclean)
-
-# WARNING
-#
-# This Makefile has been automagically generated by coq_makefile
-# Edit at your own risks !
-#
-# END OF WARNING
-