ajout option , Exc --> option, et lemmes dans les theories

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

1 files changed, 343 insertions, 0 deletions

diff --git a/theories/Num/Makefile b/theories/Num/Makefile
new file mode 100644
index 000000000..fdbe44bb6
--- /dev/null
+++ b/theories/Num/Makefile
@@ -0,0 +1,343 @@
+##############################################################################
+##                 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
+