From 8bddc438fa3a393a799c388843e235e2a63160fb Mon Sep 17 00:00:00 2001
From: letouzey
Date: Thu, 13 Dec 2007 16:17:16 +0000
Subject: migration of ide/utf8.v to theories/Unicode/Utf8.v

These notations aren't CoqIDE-specific, I can now use them with
ProofGeneral (after a small modification of PG, contact me if you're
interested by the patch). So let's place this file in a globally
visible subdir of theories/. By the way, the filename is now uppercase
as all other .v files. 

By the way, minor other changes in Makefile : extraction/test doesn't
exist anymore, and tags / otags can be made without re-doing any find.
NB: be sure to use etags that comes from emacs and not the one of 
exuberant-ctags, since the latter has now a different syntax 
(in debian, see update-alternatives etags). 



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

(limited to 'Makefile.common')

diff --git a/Makefile.common b/Makefile.common
index f2148494fa..9f035453e2 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -703,11 +703,13 @@ NUMBERSVO:=$(NATURALVO) $(INTEGERVO)
 
 SETOIDSVO:= theories/Setoids/Setoid_tac.vo theories/Setoids/Setoid_Prop.vo theories/Setoids/Setoid.vo
 
+UNICODEVO:= theories/Unicode/Utf8.vo
+
 THEORIESVO:=\
   $(INITVO) $(LOGICVO) $(ARITHVO) $(BOOLVO) $(NARITHVO) $(ZARITHVO) \
   $(SETOIDSVO) $(LISTSVO) $(STRINGSVO) $(SETSVO) $(FSETSVO) $(INTMAPVO) \
   $(RELATIONSVO) $(WELLFOUNDEDVO) $(REALSVO)  $(SORTINGVO) $(QARITHVO) \
-  $(INTSVO) $(NUMBERSVO)
+  $(INTSVO) $(NUMBERSVO) $(UNICODEVO)
 
 THEORIESLIGHTVO:= $(INITVO) $(LOGICVO) $(ARITHVO)
 
@@ -774,8 +776,6 @@ LIBFILESLIGHT:=$(THEORIESLIGHTVO)
 
 ## Specials
 
-COQIDEVO:=ide/utf8.vo
-
 INTERFACEVO:=
 
 
-- 
cgit v1.2.3