From b1dab9e06d9a964b1dd0d09bca797cb4a4e4b9a1 Mon Sep 17 00:00:00 2001
From: filliatr
Date: Tue, 21 Mar 2000 18:53:42 +0000
Subject:  - bug make_module_marker (plus de # et de .obj maintenant)  -
 portage (partiel) de Zarith  - bug discrEverywhere (manquait un "fun gls ->")

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

(limited to 'Makefile')

diff --git a/Makefile b/Makefile
index 87cc1608d9..afc8101e14 100644
--- a/Makefile
+++ b/Makefile
@@ -109,7 +109,7 @@ TOPLEVEL=toplevel/himsg.cmo toplevel/errors.cmo toplevel/vernacinterp.cmo \
          toplevel/usage.cmo toplevel/coqinit.cmo toplevel/coqtop.cmo
 
 HIGHTACTICS=tactics/dhyp.cmo tactics/auto.cmo tactics/equality.cmo \
-            tactics/tauto.cmo
+            tactics/tauto.cmo 
 
 CMA=$(CLIBS) $(CAMLP4OBJS)
 CMXA=$(CMA:.cma=.cmxa)
@@ -200,7 +200,7 @@ INITVO=theories/Init/Datatypes.vo         theories/Init/Peano.vo         \
 theories/Init/%.vo: theories/Init/%.v states/barestate.coq
 	$(COQC) -q -I theories/Init -is states/barestate.coq $<
 
-TACTICSVO=tactics/Equality.vo tactics/Tauto.vo
+TACTICSVO=tactics/Equality.vo tactics/Tauto.vo tactics/Inv.vo
 
 tactics/%.vo: tactics/%.v states/barestate.coq
 	$(COQC) -q -I tactics -is states/barestate.coq $<
-- 
cgit v1.2.3