diff options
| author | clrenard | 2001-06-12 16:20:31 +0000 |
|---|---|---|
| committer | clrenard | 2001-06-12 16:20:31 +0000 |
| commit | 2c58ecd5370c6b375b4933082d39bf76519d94f1 (patch) | |
| tree | e61c587d7c1cb9fa7d28a4b89ebda4e6f89907a4 /Makefile | |
| parent | 8e6b70111512b0ec60bd7f9a656207f03252c609 (diff) | |
Ajout des entrees puor Setoid_replace.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1783 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 13 |
1 files changed, 9 insertions, 4 deletions
@@ -41,7 +41,7 @@ LOCALINCLUDES=-I config -I tools -I scripts -I lib -I kernel -I library \ -I proofs -I tactics -I pretyping -I parsing -I toplevel \ -I contrib/omega -I contrib/ring -I contrib/xml \ -I contrib/extraction -I contrib/correctness \ - -I contrib/interface -I contrib/fourier + -I contrib/interface -I contrib/fourier -I contrib/setoid INCLUDES=$(LOCALINCLUDES) -I $(CAMLP4LIB) @@ -195,7 +195,8 @@ PARSERREQUIRES=lib/pp_control.cmo lib/pp.cmo \ ML4FILES += contrib/correctness/psyntax.ml4 contrib/field/field.ml4 CONTRIB=contrib/omega/omega.cmo contrib/omega/coq_omega.cmo \ - contrib/ring/quote.cmo contrib/ring/ring.cmo contrib/field/field.cmo \ + contrib/setoid/setoid_replace.cmo contrib/ring/quote.cmo \ + contrib/ring/ring.cmo contrib/field/field.cmo \ contrib/xml/xml.cmo \ contrib/xml/xmlcommand.cmo contrib/xml/xmlentries.cmo \ contrib/fourier/fourier.cmo contrib/fourier/fourierR.cmo \ @@ -473,6 +474,8 @@ FIELDVO = contrib/field/Field_Compl.vo contrib/field/Field_Theory.vo \ XMLVO = contrib/xml/Xml.vo +SETOIDVO = contrib/setoid/Setoid_replace.vo + INTERFACEV0 = contrib/interface/Centaur.vo contrib/interface/vernacrc FOURIERVO = contrib/fourier/Fourier_util.vo contrib/fourier/Fourier.vo @@ -483,13 +486,14 @@ contrib/interface/Centaur.vo: contrib/interface/Centaur.v $(INTERFACE) contrib/interface/AddDad.vo: contrib/interface/AddDad.v $(INTERFACE) states/initial.coq $(COQC) -boot -byte $(COQINCLUDES) $< -CONTRIBVO = $(OMEGAVO) $(RINGVO) $(FIELDVO) $(XMLVO) $(CORRECTNESSVO)\ +CONTRIBVO = $(OMEGAVO) $(SETOIDVO) $(RINGVO) $(FIELDVO) $(XMLVO) $(CORRECTNESSVO)\ $(INTERFACEV0) $(FOURIERVO) $(CONTRIBVO): states/initial.coq contrib: $(CONTRIBVO) omega: $(OMEGAVO) +setoid: $(SETOIDVO) ring: $(RINGVO) # xml_ instead of xml to avoid conflict with "make xml" xml_: $(XMLVO) @@ -649,7 +653,8 @@ LPFILES = doc/macros.tex doc/intro.tex $(LPLIB) $(LPKERNEL) $(LPLIBRARY) \ $(LPPRETYPING) $(LPPROOFS) $(LPTACTICS) $(LPTOPLEVEL) doc/coq.tex: $(LPFILES) - ocamlweb -p "\usepackage{epsfig}" $(LPFILES) -o doc/coq.tex +# ocamlweb -p "\usepackage{epsfig}" $(LPFILES) -o doc/coq.tex + ocamlweb $(LPFILES) -o doc/coq.tex clean:: rm -f doc/coq.tex |