From 2c58ecd5370c6b375b4933082d39bf76519d94f1 Mon Sep 17 00:00:00 2001
From: clrenard
Date: Tue, 12 Jun 2001 16:20:31 +0000
Subject: Ajout des entrees puor Setoid_replace.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1783 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 Makefile | 13 +++++++++----
 1 file changed, 9 insertions(+), 4 deletions(-)

(limited to 'Makefile')

diff --git a/Makefile b/Makefile
index a1db4ccebd..0191e0befa 100644
--- a/Makefile
+++ b/Makefile
@@ -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
-- 
cgit v1.2.3