diff options
| -rw-r--r-- | Makefile | 13 | ||||
| -rw-r--r-- | Makefile.build | 2 | ||||
| -rw-r--r-- | Makefile.common | 6 | ||||
| -rwxr-xr-x | configure | 2 | ||||
| -rw-r--r-- | theories/Unicode/Utf8.v (renamed from ide/utf8.v) | 2 | ||||
| -rw-r--r-- | toplevel/coqinit.ml | 1 |
6 files changed, 12 insertions, 14 deletions
@@ -171,7 +171,7 @@ archclean: clean-ide cleantheories rm -f $(MINICOQ) clean-ide: - rm -f $(COQIDEVO) $(COQIDEVO:.vo=.glob) $(COQIDECMO) $(COQIDECMX) $(COQIDECMO:.cmo=.cmi) $(COQIDEBYTE) $(COQIDEOPT) $(COQIDE) + rm -f $(COQIDECMO) $(COQIDECMX) $(COQIDECMO:.cmo=.cmi) $(COQIDEBYTE) $(COQIDEOPT) $(COQIDE) rm -f ide/extract_index.ml ide/find_phrase.ml ide/highlight.ml rm -f ide/config_lexer.ml ide/config_parser.mli ide/config_parser.ml rm -f ide/utf8_convert.ml @@ -198,10 +198,8 @@ cleantheories: # Emacs tags ########################################################################### -# NB: the -maxdepth 3 is for excluding files from contrib/extraction/test - tags: - find . -maxdepth 3 -regex ".*\.ml[i4]?" | sort -r | xargs \ + echo $(MLIFILES) $(MLFILES) $(ML4FILES) | sort -r | xargs \ etags --language=none\ "--regex=/let[ \t]+\([^ \t]+\)/\1/" \ "--regex=/let[ \t]+rec[ \t]+\([^ \t]+\)/\1/" \ @@ -210,15 +208,14 @@ tags: "--regex=/exception[ \t]+\([^ \t]+\)/\1/" \ "--regex=/val[ \t]+\([^ \t]+\)/\1/" \ "--regex=/module[ \t]+\([^ \t]+\)/\1/" - find . -maxdepth 3 -name "*.ml4" | sort -r | xargs \ + echo $(ML4FILES) | sort -r | xargs \ etags --append --language=none\ "--regex=/[ \t]*\([^: \t]+\)[ \t]*:/\1/" otags: - find . -maxdepth 3 -name "*.ml" -o -name "*.mli" \ - | sort -r | xargs otags - find . -maxdepth 3 -name "*.ml4" | sort -r | xargs \ + echo $(MLIFILES) $(MLFILES) | sort -r | xargs otags + echo $(ML4FILES) | sort -r | xargs \ etags --append --language=none\ "--regex=/let[ \t]+\([^ \t]+\)/\1/" \ "--regex=/let[ \t]+rec[ \t]+\([^ \t]+\)/\1/" \ diff --git a/Makefile.build b/Makefile.build index 3865ce1e2..0674e5bba 100644 --- a/Makefile.build +++ b/Makefile.build @@ -328,7 +328,7 @@ COQIDEFLAGS=-thread $(COQIDEINCLUDES) .SUFFIXES:.vo -IDEFILES=$(COQIDEVO) ide/utf8.v ide/coq.png ide/.coqide-gtk2rc +IDEFILES=ide/coq.png ide/.coqide-gtk2rc coqide-binaries: coqide-$(HASCOQIDE) coqide-no: diff --git a/Makefile.common b/Makefile.common index f2148494f..9f035453e 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:= @@ -766,7 +766,7 @@ PRINTF=`which printf` # Subdirectories of theories/ added in coq_config.ml subdirs () { - (cd $1; find * \( -name .svn -prune \) -o \( -type d -exec $PRINTF "\"%s\";\n" {} \; \) | grep -v extraction/test | grep -v correctness >> "$mlconfig_file") + (cd $1; find * \( -name .svn -prune \) -o \( -type d -exec $PRINTF "\"%s\";\n" {} \; \) | grep -v correctness >> "$mlconfig_file") } echo "let theories_dirs = [" >> "$mlconfig_file" diff --git a/ide/utf8.v b/theories/Unicode/Utf8.v index db7da402c..0a0a3b95d 100644 --- a/ide/utf8.v +++ b/theories/Unicode/Utf8.v @@ -51,6 +51,6 @@ Goal ∀ x, True -> (∃ y , x ≥ y + 1) ∨ x ≤ 0. *) (* Integer Arithmetic *) -(* TODO +(* TODO: this should come after ZArith Notation "x ≤ y" := (Zle x y) (at level 1, y at level 10). *) diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index 9f301d3a4..8d9eabd7e 100644 --- a/toplevel/coqinit.ml +++ b/toplevel/coqinit.ml @@ -70,6 +70,7 @@ let hm2 s = (* The list of all theories in the standard library /!\ order does matter *) let theories_dirs_map = [ + "theories/Unicode", "Unicode" ; "theories/Program", "Program" ; "theories/FSets", "FSets" ; "theories/IntMap", "IntMap" ; |