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 | 13 +++++------- Makefile.build | 2 +- Makefile.common | 6 +++--- configure | 2 +- ide/utf8.v | 56 ------------------------------------------------- theories/Unicode/Utf8.v | 56 +++++++++++++++++++++++++++++++++++++++++++++++++ toplevel/coqinit.ml | 1 + 7 files changed, 67 insertions(+), 69 deletions(-) delete mode 100644 ide/utf8.v create mode 100644 theories/Unicode/Utf8.v diff --git a/Makefile b/Makefile index 51a679ac7f..dabe3078c6 100644 --- a/Makefile +++ b/Makefile @@ -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 3865ce1e23..0674e5bbac 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 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:= diff --git a/configure b/configure index a8891856d1..b00c259260 100755 --- a/configure +++ b/configure @@ -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/ide/utf8.v deleted file mode 100644 index db7da402cc..0000000000 --- a/ide/utf8.v +++ /dev/null @@ -1,56 +0,0 @@ -(* -*- coding:utf-8 -* *) -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* y) (at level 90, right associativity): type_scope. -Notation "x ↔ y" := (x <-> y) (at level 95, no associativity): type_scope. -Notation "⌉ x" := (~x) (at level 75, right associativity) : type_scope. -Notation "x ≠ y" := (x <> y) (at level 70) : type_scope. - -(* Abstraction *) -(* Not nice -Notation "'λ' x : T , y" := ([x:T] y) (at level 1, x,T,y at level 10). -Notation "'λ' x := T , y" := ([x:=T] y) (at level 1, x,T,y at level 10). -*) - -(* Arithmetic *) -Notation "x ≤ y" := (le x y) (at level 70, no associativity). -Notation "x ≥ y" := (ge x y) (at level 70, no associativity). - -(* test *) -(* -Goal ∀ x, True -> (∃ y , x ≥ y + 1) ∨ x ≤ 0. -*) - -(* Integer Arithmetic *) -(* TODO -Notation "x ≤ y" := (Zle x y) (at level 1, y at level 10). -*) diff --git a/theories/Unicode/Utf8.v b/theories/Unicode/Utf8.v new file mode 100644 index 0000000000..0a0a3b95db --- /dev/null +++ b/theories/Unicode/Utf8.v @@ -0,0 +1,56 @@ +(* -*- coding:utf-8 -* *) +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* y) (at level 90, right associativity): type_scope. +Notation "x ↔ y" := (x <-> y) (at level 95, no associativity): type_scope. +Notation "⌉ x" := (~x) (at level 75, right associativity) : type_scope. +Notation "x ≠ y" := (x <> y) (at level 70) : type_scope. + +(* Abstraction *) +(* Not nice +Notation "'λ' x : T , y" := ([x:T] y) (at level 1, x,T,y at level 10). +Notation "'λ' x := T , y" := ([x:=T] y) (at level 1, x,T,y at level 10). +*) + +(* Arithmetic *) +Notation "x ≤ y" := (le x y) (at level 70, no associativity). +Notation "x ≥ y" := (ge x y) (at level 70, no associativity). + +(* test *) +(* +Goal ∀ x, True -> (∃ y , x ≥ y + 1) ∨ x ≤ 0. +*) + +(* Integer Arithmetic *) +(* 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 9f301d3a4b..8d9eabd7ef 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" ; -- cgit v1.2.3