Move CoqIDE to its own folder

The will make it possible to put a VsCoq toplevel in `ide/vscoq`.

115 files changed, 62 insertions, 62 deletions

diff --git a/.gitignore b/.gitignore
index adbf9dd189..0c7a8f70f6 100644
--- a/.gitignore
+++ b/.gitignore
@@ -121,14 +121,14 @@ doc/unreleased.rst
 
 coqpp/coqpp_lex.ml
 dev/ocamlweb-doc/lex.ml
-ide/coq_lex.ml
-ide/config_lexer.ml
-ide/utf8_convert.ml
+ide/coqide/coq_lex.ml
+ide/coqide/config_lexer.ml
+ide/coqide/utf8_convert.ml
 tools/coqwc.ml
 tools/coqdep_lexer.ml
 tools/ocamllibdep.ml
 tools/coqdoc/cpretty.ml
-ide/protocol/xml_lexer.ml
+ide/coqide/protocol/xml_lexer.ml
 
 # .mly files
 
@@ -143,7 +143,7 @@ plugins/ltac/coretactics.ml
 plugins/ltac/extratactics.ml
 plugins/ltac/extraargs.ml
 plugins/ltac/profile_ltac_tactics.ml
-ide/coqide_os_specific.ml
+ide/coqide/coqide_os_specific.ml
 plugins/ssrmatching/ssrmatching.ml
 plugins/ssr/ssrparser.ml
 plugins/ssr/ssrvernac.ml
@@ -155,9 +155,9 @@ kernel/byterun/coq_jumptbl.h
 kernel/genOpcodeFiles.exe
 kernel/copcodes.ml
 kernel/uint63.ml
-ide/default.bindings
-ide/default_bindings_src.exe
-ide/index_urls.txt
+ide/coqide/default.bindings
+ide/coqide/default_bindings_src.exe
+ide/coqide/index_urls.txt
 .lia.cache
 .nia.cache
 
@@ -187,4 +187,4 @@ META.coq
 *.install
 !Makefile.install
 
-ide/coqide.keys
+ide/coqide/coqide.keys
diff --git a/Makefile.build b/Makefile.build
index 3140df4cee..7806dce79c 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -254,7 +254,7 @@ OCAMLOPT = $(TIMER) $(OCAMLFIND) opt $(CAMLFLAGS)
 
 BYTEFLAGS=$(CAMLDEBUG) $(USERFLAGS)
 OPTFLAGS=$(CAMLDEBUGOPT) $(CAMLTIMEPROF) $(USERFLAGS) $(FLAMBDA_FLAGS)
-DEPFLAGS=$(LOCALINCLUDES) -map gramlib/.pack/gramlib.ml $(if $(filter plugins/% user-contrib/%,$@),, -I ide -I ide/protocol)
+DEPFLAGS=$(LOCALINCLUDES) -map gramlib/.pack/gramlib.ml $(if $(filter plugins/% user-contrib/%,$@),, -I ide/coqide -I ide/coqide/protocol)
 
 # On MacOS, the binaries are signed, except our private ones
 ifeq ($(shell which codesign > /dev/null 2>&1 && echo $(ARCH)),Darwin)
@@ -555,15 +555,15 @@ $(COQWORKMGRBYTE): $(COQWORKMGRCMO)
 # fake_ide : for debugging or test-suite purpose, a fake ide simulating
 # a connection to coqidetop
 
-FAKEIDECMO:=config/config.cma clib/clib.cma lib/lib.cma ide/protocol/ideprotocol.cma ide/document.cmo ide/fake_ide.cmo
+FAKEIDECMO:=config/config.cma clib/clib.cma lib/lib.cma ide/coqide/protocol/ideprotocol.cma ide/coqide/document.cmo ide/coqide/fake_ide.cmo
 
 $(FAKEIDE): $(call bestobj, $(FAKEIDECMO)) | $(IDETOPEXE)
 	$(SHOW)'OCAMLBEST -o $@'
-	$(HIDE)$(call bestocaml, -I ide -I ide/protocol -package str -package dynlink)
+	$(HIDE)$(call bestocaml, -I ide/coqide -I ide/coqide/protocol -package str -package dynlink)
 
 $(FAKEIDEBYTE): $(FAKEIDECMO) | $(IDETOPBYTE)
 	$(SHOW)'OCAMLC -o $@'
-	$(HIDE)$(call ocamlbyte, -I ide -package str,unix,threads)
+	$(HIDE)$(call ocamlbyte, -I ide/coqide -package str,unix,threads)
 
 # votour: a small vo explorer (based on the checker)
 
@@ -692,7 +692,7 @@ kernel/kernel.cmxa: kernel/kernel.mllib
 	$(SHOW)'OCAMLOPT -pack -o $@'
 	$(HIDE)$(OCAMLOPT) $(MLINCLUDES) $(OPTFLAGS) -pack -o $@ $(filter-out %.mlpack, $^)
 
-COND_IDEFLAGS=$(if $(filter ide/fake_ide% tools/coq_makefile%,$<), -I ide -I ide/protocol,)
+COND_IDEFLAGS=$(if $(filter ide/coqide/fake_ide% tools/coq_makefile%,$<), -I ide/coqide -I ide/coqide/protocol,)
 COND_PRINTERFLAGS=$(if $(filter dev/%,$<), -I dev,)
 
 COND_GRAMFLAGS=$(if $(filter gramlib/.pack/%,$<),-no-alias-deps -w -49,) $(if $(filter gramlib/.pack/gramlib__%,$<),-open Gramlib,)
diff --git a/Makefile.ide b/Makefile.ide
index ef9d67d4ec..640ee7b188 100644
--- a/Makefile.ide
+++ b/Makefile.ide
@@ -13,13 +13,13 @@
 ## NB: For the moment, the build system of CoqIDE is part of
 ## the one of Coq. In particular, this Makefile.ide is included in
 ## Makefile.build. Please ensure that the rules define here are
-## indeed specific to files of the form ide/*
+## indeed specific to files of the form ide/coqide/*
 
 ## Coqide-related variables set by ./configure in config/Makefile
 
 #HASCOQIDE : opt / byte / no
 #IDEFLAGS : some extra cma, for instance
-#IDEOPTCDEPS : on windows, ide/ide_win32_stubs.o ide/coq_icon.o
+#IDEOPTCDEPS : on windows, ide/coqide/ide_win32_stubs.o ide/coqide/coq_icon.o
 #IDECDEPS
 #IDECDEPSFLAGS
 #IDEINT : X11 / QUARTZ / WIN32
@@ -34,11 +34,11 @@ COQIDEINAPP:=$(COQIDEAPP)/Contents/MacOS/coqide
 ## CoqIDE source directory and files
 
 # Note : for just building bin/coqide, we could only consider
-# config, lib, ide and ide/utils. But the coqidetop plugin (the
+# config, lib, ide/coqide and ide/coqide/utils. But the coqidetop plugin (the
 # one that will be loaded by coqidetop) refers to some
 # core modules of coq, for instance printing/*.
 
-IDESRCDIRS:= $(CORESRCDIRS) ide ide/protocol
+IDESRCDIRS:= $(CORESRCDIRS) ide/coqide ide/coqide/protocol
 
 ifeq ($(HASCOQIDE),no)
 COQIDEFLAGS=$(addprefix -I , $(IDESRCDIRS))
@@ -46,20 +46,20 @@ else
 COQIDEFLAGS=$(addprefix -I , $(IDESRCDIRS)) -package lablgtk3-sourceview3
 endif
 
-IDEDEPS:=config/config.cma clib/clib.cma lib/lib.cma ide/protocol/ideprotocol.cma
-IDECMA:=ide/ide.cma
+IDEDEPS:=config/config.cma clib/clib.cma lib/lib.cma ide/coqide/protocol/ideprotocol.cma
+IDECMA:=ide/coqide/ide.cma
 IDETOPEXE=bin/coqidetop$(EXE)
 IDETOP=bin/coqidetop.opt$(EXE)
 IDETOPBYTE=bin/coqidetop.byte$(EXE)
 
-LINKIDE:=$(IDEDEPS) $(IDECDEPS) $(IDECMA) ide/coqide_os_specific.cmo ide/coqide_main.mli ide/coqide_main.ml
-LINKIDEOPT:=$(IDEOPTCDEPS) $(patsubst %.cma,%.cmxa,$(IDEDEPS:.cmo=.cmx)) $(IDECMA:.cma=.cmxa) ide/coqide_os_specific.cmx ide/coqide_main.mli ide/coqide_main.ml
+LINKIDE:=$(IDEDEPS) $(IDECDEPS) $(IDECMA) ide/coqide/coqide_os_specific.cmo ide/coqide/coqide_main.mli ide/coqide/coqide_main.ml
+LINKIDEOPT:=$(IDEOPTCDEPS) $(patsubst %.cma,%.cmxa,$(IDEDEPS:.cmo=.cmx)) $(IDECMA:.cma=.cmxa) ide/coqide/coqide_os_specific.cmx ide/coqide/coqide_main.mli ide/coqide/coqide_main.ml
 
-IDEBINDINGS:=ide/default.bindings
-IDEBINDINGSSRC:=ide/default_bindings_src.ml
-IDEBINDINGSEXE:=ide/default_bindings_src.exe
+IDEBINDINGS:=ide/coqide/default.bindings
+IDEBINDINGSSRC:=ide/coqide/default_bindings_src.ml
+IDEBINDINGSEXE:=ide/coqide/default_bindings_src.exe
 
-IDEFILES=$(wildcard ide/*.lang) ide/coq_style.xml ide/coq.png $(IDEBINDINGS)
+IDEFILES=$(wildcard ide/coqide/*.lang) ide/coqide/coq_style.xml ide/coqide/coq.png $(IDEBINDINGS)
 
 ## GTK for Coqide MacOS bundle
 
@@ -118,49 +118,49 @@ $(COQIDEBYTE): $(LINKIDE)
 	$(HIDE)$(OCAMLC) $(COQIDEFLAGS) $(BYTEFLAGS) -o $@ \
 	       -linkpkg -package str,unix,threads,lablgtk3-sourceview3 $(IDEFLAGS) $(IDECDEPSFLAGS) $^
 
-ide/coqide_os_specific.ml: ide/coqide_$(IDEINT).ml.in config/Makefile
+ide/coqide/coqide_os_specific.ml: ide/coqide/coqide_$(IDEINT).ml.in config/Makefile
 	rm -f $@ && cp $< $@ && chmod a-w $@
 
-ide/%.cmi: ide/%.mli
+ide/coqide/%.cmi: ide/coqide/%.mli
 	$(SHOW)'OCAMLC    $<'
 	$(HIDE)$(OCAMLC) $(COQIDEFLAGS) $(BYTEFLAGS) -c $<
 
-ide/%.cmo: ide/%.ml
+ide/coqide/%.cmo: ide/coqide/%.ml
 	$(SHOW)'OCAMLC    $<'
 	$(HIDE)$(OCAMLC) $(COQIDEFLAGS) $(BYTEFLAGS) -c $<
 
-ide/%.cmx: ide/%.ml
+ide/coqide/%.cmx: ide/coqide/%.ml
 	$(SHOW)'OCAMLOPT  $<'
 	$(HIDE)$(OCAMLOPT) $(COQIDEFLAGS) $(OPTFLAGS) -c $<
 
 # We need to compile this file without -safe-string due mess with
 # lablgtk API. Other option is to require lablgtk >= 3.0.0
-ide/ideutils.cmo: ide/ideutils.ml
+ide/coqide/ideutils.cmo: ide/coqide/ideutils.ml
 	$(SHOW)'OCAMLC    $<'
 	$(HIDE)$(filter-out -safe-string,$(OCAMLC)) $(COQIDEFLAGS) $(BYTEFLAGS) -c $<
 
-ide/ideutils.cmx: ide/ideutils.ml
+ide/coqide/ideutils.cmx: ide/coqide/ideutils.ml
 	$(SHOW)'OCAMLOPT  $<'
 	$(HIDE)$(filter-out -safe-string,$(OCAMLOPT)) $(COQIDEFLAGS) $(filter-out -safe-string,$(OPTFLAGS)) -c $<
 
-IDETOPCMA:=ide/ide_common.cma
+IDETOPCMA:=ide/coqide/ide_common.cma
 IDETOPCMX:=$(IDETOPCMA:.cma=.cmxa)
 
 # Special rule for coqidetop
 $(IDETOPEXE): $(IDETOP:.opt=.$(BEST))
 	rm -f $@ && cp $< $@
 
-$(IDETOP): ide/idetop.ml $(LINKCMX) $(LIBCOQRUN) $(IDETOPCMX)
+$(IDETOP): ide/coqide/idetop.ml $(LINKCMX) $(LIBCOQRUN) $(IDETOPCMX)
 	$(SHOW)'COQMKTOP -o $@'
-	$(HIDE)$(OCAMLOPT) -linkall -linkpkg $(MLINCLUDES) -I ide -I ide/protocol/ \
+	$(HIDE)$(OCAMLOPT) -linkall -linkpkg $(MLINCLUDES) -I ide/coqide -I ide/coqide/protocol/ \
 			   $(SYSMOD) \
 			   $(LINKCMX) $(IDETOPCMX) $(OPTFLAGS) $(LINKMETADATA) $< -o $@
 	$(STRIP_HIDE) $@
 	$(CODESIGN_HIDE) $@
 
-$(IDETOPBYTE): ide/idetop.ml $(LINKCMO) $(LIBCOQRUN) $(IDETOPCMA)
+$(IDETOPBYTE): ide/coqide/idetop.ml $(LINKCMO) $(LIBCOQRUN) $(IDETOPCMA)
 	$(SHOW)'COQMKTOP -o $@'
-	$(HIDE)$(OCAMLC) -linkall -linkpkg $(MLINCLUDES) -I ide -I ide/protocol/ \
+	$(HIDE)$(OCAMLC) -linkall -linkpkg $(MLINCLUDES) -I ide/coqide -I ide/coqide/protocol/ \
 	                 -I kernel/byterun/ -cclib -lcoqrun $(VMBYTEFLAGS) \
 			 $(SYSMOD) \
 			 $(LINKCMO) $(IDETOPCMA) $(BYTEFLAGS) $< -o $@
@@ -219,12 +219,12 @@ endif
 
 install-ide-files: #Please update $(COQIDEAPP)/Contents/Resources/ at the same time
 	$(MKDIR) $(FULLDATADIR)
-	$(INSTALLLIB) ide/coq.png ide/*.lang ide/coq_style.xml $(IDEBINDINGS) $(FULLDATADIR)
+	$(INSTALLLIB) ide/coqide/coq.png ide/coqide/*.lang ide/coqide/coq_style.xml $(IDEBINDINGS) $(FULLDATADIR)
 	$(MKDIR) $(FULLCONFIGDIR)
 
 install-ide-info:
 	$(MKDIR) $(FULLDOCDIR)
-	$(INSTALLLIB) ide/FAQ $(FULLDOCDIR)/FAQ-CoqIde
+	$(INSTALLLIB) ide/coqide/FAQ $(FULLDOCDIR)/FAQ-CoqIde
 
 ###########################################################################
 # CoqIde MacOS special targets
@@ -235,10 +235,10 @@ install-ide-info:
 $(COQIDEAPP)/Contents:
 	rm -rdf $@
 	$(MKDIR) $@
-	sed -e "s/VERSION/$(VERSION4MACOS)/g" ide/MacOS/Info.plist.template > $@/Info.plist
+	sed -e "s/VERSION/$(VERSION4MACOS)/g" ide/coqide/MacOS/Info.plist.template > $@/Info.plist
 	$(MKDIR) "$@/MacOS"
 
-$(COQIDEINAPP): ide/macos_prehook.cmx $(LINKIDEOPT) | $(COQIDEAPP)/Contents
+$(COQIDEINAPP): ide/coqide/macos_prehook.cmx $(LINKIDEOPT) | $(COQIDEAPP)/Contents
 	$(SHOW)'OCAMLOPT -o $@'
 	$(HIDE)$(OCAMLOPT) $(COQIDEFLAGS) $(OPTFLAGS) -o $@ \
 	        -linkpkg -package str,unix,threads,lablgtk3-sourceview3 $(IDEFLAGS:.cma=.cmxa) $^
@@ -246,7 +246,7 @@ $(COQIDEINAPP): ide/macos_prehook.cmx $(LINKIDEOPT) | $(COQIDEAPP)/Contents
 
 $(COQIDEAPP)/Contents/Resources/share: $(COQIDEAPP)/Contents
 	$(MKDIR) $@/coq/
-	$(INSTALLLIB) ide/coq.png ide/*.lang ide/coq_style.xml $(IDEBINDINGS) $@/coq/
+	$(INSTALLLIB) ide/coqide/coq.png ide/coqide/*.lang ide/coqide/coq_style.xml $(IDEBINDINGS) $@/coq/
 	$(MKDIR) $@/gtksourceview-3.0/{language-specs,styles}
 	$(INSTALLLIB) "$(SOURCEVIEWSHARE)/"gtksourceview-3.0/language-specs/{def.lang,language2.rng} $@/gtksourceview-3.0/language-specs/
 	$(INSTALLLIB) "$(SOURCEVIEWSHARE)/"gtksourceview-3.0/styles/{styles.rng,classic.xml} $@/gtksourceview-3.0/styles/
@@ -287,7 +287,7 @@ $(COQIDEAPP)/Contents/Resources/lib: $(COQIDEAPP)/Contents/Resources/immodules $
 	done
 
 $(COQIDEAPP)/Contents/Resources:$(COQIDEAPP)/Contents/Resources/etc $(COQIDEAPP)/Contents/Resources/share
-	$(INSTALLLIB) ide/MacOS/*.icns $@
+	$(INSTALLLIB) ide/coqide/MacOS/*.icns $@
 
 $(COQIDEAPP):$(COQIDEAPP)/Contents/Resources
 	$(CODESIGN_HIDE) $@
diff --git a/Makefile.install b/Makefile.install
index cc0888d8e4..4977bb38e1 100644
--- a/Makefile.install
+++ b/Makefile.install
@@ -91,12 +91,12 @@ install-tools:
 # - the ones corresponding to packed plugins
 
 INSTALLCMI = $(sort \
-	$(filter-out checker/% ide/% tools/%, $(MLIFILES:.mli=.cmi)) \
+	$(filter-out checker/% ide/coqide/% tools/%, $(MLIFILES:.mli=.cmi)) \
 	$(GRAMMLIFILES:.mli=.cmi) gramlib/.pack/gramlib.cmi \
 	$(foreach lib,$(CORECMA), $(addsuffix .cmi,$($(lib:.cma=_MLLIB_DEPENDENCIES))))) \
 	$(PLUGINS:.cmo=.cmi)
 
-INSTALLCMX = $(sort $(filter-out checker/% ide/% tools/% dev/% \
+INSTALLCMX = $(sort $(filter-out checker/% ide/coqide/% tools/% dev/% \
 	configure.cmx toplevel/coqtop_byte_bin.cmx plugins/extraction/big.cmx, \
 	$(GRAMMLFILES:.ml=.cmx) $(MLFILES:.ml=.cmx)))
 
diff --git a/Makefile.make b/Makefile.make
index 2a0a58756c..7191738612 100644
--- a/Makefile.make
+++ b/Makefile.make
@@ -107,7 +107,7 @@ GRAMMLIFILES := $(addsuffix .mli, $(GRAMFILES))
 GENGRAMMLFILES := $(GRAMMLFILES) gramlib/.pack/gramlib.ml # why is gramlib.ml not in GRAMMLFILES?
 
 GENMLGFILES:= $(MLGFILES:.mlg=.ml)
-GENMLFILES:=$(LEXFILES:.mll=.ml) $(YACCFILES:.mly=.ml) $(GENMLGFILES) $(GENGRAMMLFILES) ide/coqide_os_specific.ml kernel/copcodes.ml kernel/uint63.ml
+GENMLFILES:=$(LEXFILES:.mll=.ml) $(YACCFILES:.mly=.ml) $(GENMLGFILES) $(GENGRAMMLFILES) ide/coqide/coqide_os_specific.ml kernel/copcodes.ml kernel/uint63.ml
 GENMLIFILES:=$(GRAMMLIFILES)
 GENHFILES:=kernel/byterun/coq_instruct.h kernel/byterun/coq_jumptbl.h
 GENFILES:=$(GENMLFILES) $(GENMLIFILES) $(GENHFILES) kernel/genOpcodeFiles.exe
@@ -262,10 +262,10 @@ optclean:
 
 clean-ide:
 	rm -f $(COQIDECMO) $(COQIDECMX) $(COQIDECMO:.cmo=.cmi) $(COQIDEBYTE) $(COQIDE)
-	rm -f ide/input_method_lexer.ml
-	rm -f ide/highlight.ml ide/config_lexer.ml ide/config_parser.mli ide/config_parser.ml
-	rm -f ide/utf8_convert.ml
-	rm -f ide/default.bindings ide/default_bindings_src.exe
+	rm -f ide/coqide/input_method_lexer.ml
+	rm -f ide/coqide/highlight.ml ide/coqide/config_lexer.ml ide/coqide/config_parser.mli ide/coqide/config_parser.ml
+	rm -f ide/coqide/utf8_convert.ml
+	rm -f ide/coqide/default.bindings ide/coqide/default_bindings_src.exe
 	rm -rf $(COQIDEAPP)
 
 mlgclean:
diff --git a/configure.ml b/configure.ml
index 9cfa9d409e..c05844198b 100644
--- a/configure.ml
+++ b/configure.ml
@@ -81,7 +81,7 @@ let read_lines_and_close fd =
 (** Run some unix command and read the first line of its output.
     We avoid Unix.open_process and its non-fully-portable /bin/sh,
     especially when it comes to quoting the filenames.
-    See open_process_pid in ide/coq.ml for more details.
+    See open_process_pid in ide/coqide/coq.ml for more details.
     Error messages:
      - if err=StdErr, any error message goes in the stderr of our script.
      - if err=StdOut, we merge stderr and stdout (just as 2>&1).
@@ -784,7 +784,7 @@ let coqide_flags () =
         idearchdef := "QUARTZ"
       end
     | "opt", "win32" ->
-      idearchfile := "ide/ide_win32_stubs.o ide/coq_icon.o";
+      idearchfile := "ide/coqide/ide_win32_stubs.o ide/coqide/coq_icon.o";
       idecdepsflags := "-custom";
       idearchflags := "-ccopt '-subsystem windows'";
       idearchdef := "WIN32"
@@ -847,9 +847,9 @@ let install = [
   "COQLIBINSTALL", "the Coq library", !prefs.libdir,
     Relative "lib", Relative "lib/coq", Relative "";
   "CONFIGDIR", "the Coqide configuration files", !prefs.configdir,
-    Relative "config", Absolute "/etc/xdg/coq", Relative "ide";
+    Relative "config", Absolute "/etc/xdg/coq", Relative "ide/coqide";
   "DATADIR", "the Coqide data files", !prefs.datadir,
-    Relative "share", Relative "share/coq", Relative "ide";
+    Relative "share", Relative "share/coq", Relative "ide/coqide";
   "MANDIR", "the Coq man pages", !prefs.mandir,
     Relative "man", Relative "share/man", Relative "man";
   "DOCDIR", "the Coq documentation", !prefs.docdir,
diff --git a/dev/build/windows/ReadMe.txt b/dev/build/windows/ReadMe.txt
index 052014824f..f34bbea4e9 100644
--- a/dev/build/windows/ReadMe.txt
+++ b/dev/build/windows/ReadMe.txt
@@ -423,7 +423,7 @@ Binary file ./bin/ocpp5.exe matches
 Binary file ./lib/config/coq_config.cmo matches
 Binary file ./lib/config/coq_config.o matches
 Binary file ./lib/grammar/grammar.cma matches
-Binary file ./lib/ide/ide_win32_stubs.o matches
+Binary file ./lib/ide/coqide/ide_win32_stubs.o matches
 Binary file ./lib/lib/clib.a matches
 Binary file ./lib/lib/clib.cma matches
 Binary file ./lib/libcoqrun.a matches
diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh
index 963b0e6387..ba552ab302 100755
--- a/dev/build/windows/makecoq_mingw.sh
+++ b/dev/build/windows/makecoq_mingw.sh
@@ -1303,11 +1303,11 @@ function copy_coq_gtk {
     install -D -T "$PREFIXMINGW/share/glib-2.0/schemas/gschemas.compiled"        "$PREFIXCOQ/share/glib-2.0/schemas/gschemas.compiled"
 
     install_glob  "$PREFIXMINGW/share/gtksourceview-3.0/language-specs" '*'      "$PREFIXCOQ/share/gtksourceview-3.0/language-specs"
-    install -D -T "ide/coq.lang"                                                 "$PREFIXCOQ/share/gtksourceview-3.0/language-specs/coq.lang"
-    install -D -T "ide/coq-ssreflect.lang"                                       "$PREFIXCOQ/share/gtksourceview-3.0/language-specs/coq-ssreflect.lang"
+    install -D -T "ide/coqide/coq.lang"                                                 "$PREFIXCOQ/share/gtksourceview-3.0/language-specs/coq.lang"
+    install -D -T "ide/coqide/coq-ssreflect.lang"                                       "$PREFIXCOQ/share/gtksourceview-3.0/language-specs/coq-ssreflect.lang"
 
     install_glob  "$PREFIXMINGW/share/gtksourceview-3.0/styles" '*'              "$PREFIXCOQ/share/gtksourceview-3.0/styles"
-    install -D -T "ide/coq_style.xml"                                            "$PREFIXCOQ/share/gtksourceview-3.0/styles/coq_style.xml"
+    install -D -T "ide/coqide/coq_style.xml"                                            "$PREFIXCOQ/share/gtksourceview-3.0/styles/coq_style.xml"
 
     install_rec   "$PREFIXMINGW/share/themes" '*'                                "$PREFIXCOQ/share/themes"
 
@@ -1340,8 +1340,8 @@ function copy_coq_gtk {
     #   COQSHARE="$PREFIXCOQ/share/"
     # fi
 
-    # mkdir -p "$PREFIXCOQ/ide"
-    # mv "$COQSHARE"*.png  "$PREFIXCOQ/ide"
+    # mkdir -p "$PREFIXCOQ/ide/coqide"
+    # mv "$COQSHARE"*.png  "$PREFIXCOQ/ide/coqide"
     # rmdir "$PREFIXCOQ/share/coq" || true
   fi
 }
@@ -1598,7 +1598,7 @@ function make_coq_installer {
     cp ../patches/ReplaceInFile.nsh dev/nsis
     VERSION=$(grep '^VERSION=' config/Makefile | cut -d = -f 2 | tr -d '\r')
     cd dev/nsis
-    logn nsis-installer "$NSIS" -DVERSION="$VERSION" -DARCH="$ARCH" -DCOQ_SRC_PATH="$PREFIXCOQ" -DCOQ_ICON=..\\..\\ide\\coq.ico -DCOQ_ADDONS="$COQ_ADDONS" coq_new.nsi
+    logn nsis-installer "$NSIS" -DVERSION="$VERSION" -DARCH="$ARCH" -DCOQ_SRC_PATH="$PREFIXCOQ" -DCOQ_ICON=..\\..\\ide\\coqide\\coq.ico -DCOQ_ADDONS="$COQ_ADDONS" coq_new.nsi
 
     build_post
   fi
diff --git a/ide/coq_icon.rc b/ide/coq_icon.rc
deleted file mode 100644
index f873e7de11..0000000000
--- a/ide/coq_icon.rc
+++ /dev/null
@@ -1 +0,0 @@
-large   ICON    ide/coq.ico
diff --git a/ide/FAQ b/ide/coqide/FAQ
index c8b0a5d328..c8b0a5d328 100644
--- a/ide/FAQ
+++ b/ide/coqide/FAQ
diff --git a/ide/MacOS/Info.plist.template b/ide/coqide/MacOS/Info.plist.template
index e4fb0e5980..e4fb0e5980 100644
--- a/ide/MacOS/Info.plist.template
+++ b/ide/coqide/MacOS/Info.plist.template
diff --git a/ide/MacOS/coqfile.icns b/ide/coqide/MacOS/coqfile.icns
index 107e70431d..107e70431d 100644
--- a/ide/MacOS/coqfile.icns
+++ b/ide/coqide/MacOS/coqfile.icns
diff --git a/ide/MacOS/coqide.icns b/ide/coqide/MacOS/coqide.icns
index 92bdfe773f..92bdfe773f 100644
--- a/ide/MacOS/coqide.icns
+++ b/ide/coqide/MacOS/coqide.icns
diff --git a/ide/Make b/ide/coqide/Make
index c0881ca392..c0881ca392 100644
--- a/ide/Make
+++ b/ide/coqide/Make
diff --git a/ide/config_lexer.mli b/ide/coqide/config_lexer.mli
index 196192d5be..196192d5be 100644
--- a/ide/config_lexer.mli
+++ b/ide/coqide/config_lexer.mli
diff --git a/ide/config_lexer.mll b/ide/coqide/config_lexer.mll
index 4ef9a1fafd..4ef9a1fafd 100644
--- a/ide/config_lexer.mll
+++ b/ide/coqide/config_lexer.mll
diff --git a/ide/configwin.ml b/ide/coqide/configwin.ml
index 79a1eae880..79a1eae880 100644
--- a/ide/configwin.ml
+++ b/ide/coqide/configwin.ml
diff --git a/ide/configwin.mli b/ide/coqide/configwin.mli
index b5c3e74aec..b5c3e74aec 100644
--- a/ide/configwin.mli
+++ b/ide/coqide/configwin.mli
diff --git a/ide/configwin_ihm.ml b/ide/coqide/configwin_ihm.ml
index e768131dcf..e768131dcf 100644
--- a/ide/configwin_ihm.ml
+++ b/ide/coqide/configwin_ihm.ml
diff --git a/ide/configwin_ihm.mli b/ide/coqide/configwin_ihm.mli
index ce6cd4d7c1..ce6cd4d7c1 100644
--- a/ide/configwin_ihm.mli
+++ b/ide/coqide/configwin_ihm.mli
diff --git a/ide/configwin_messages.ml b/ide/coqide/configwin_messages.ml
index de1b4721d0..de1b4721d0 100644
--- a/ide/configwin_messages.ml
+++ b/ide/coqide/configwin_messages.ml
diff --git a/ide/configwin_types.ml b/ide/coqide/configwin_types.ml
index 711eccd08e..711eccd08e 100644
--- a/ide/configwin_types.ml
+++ b/ide/coqide/configwin_types.ml
diff --git a/ide/coq-ssreflect.lang b/ide/coqide/coq-ssreflect.lang
index fc7bc64a68..fc7bc64a68 100644
--- a/ide/coq-ssreflect.lang
+++ b/ide/coqide/coq-ssreflect.lang
diff --git a/ide/coq.ico b/ide/coqide/coq.ico
index 94ce897d17..94ce897d17 100644
--- a/ide/coq.ico
+++ b/ide/coqide/coq.ico
diff --git a/ide/coq.lang b/ide/coqide/coq.lang
index e9eab48de7..e9eab48de7 100644
--- a/ide/coq.lang
+++ b/ide/coqide/coq.lang
diff --git a/ide/coq.ml b/ide/coqide/coq.ml
index 57cdccce6d..57cdccce6d 100644
--- a/ide/coq.ml
+++ b/ide/coqide/coq.ml
diff --git a/ide/coq.mli b/ide/coqide/coq.mli
index 82df36c91c..82df36c91c 100644
--- a/ide/coq.mli
+++ b/ide/coqide/coq.mli
diff --git a/ide/coq.png b/ide/coqide/coq.png
index 136bfdd5fe..136bfdd5fe 100644
--- a/ide/coq.png
+++ b/ide/coqide/coq.png
diff --git a/ide/coq2.ico b/ide/coqide/coq2.ico
index bc1732fd99..bc1732fd99 100644
--- a/ide/coq2.ico
+++ b/ide/coqide/coq2.ico
diff --git a/ide/coqOps.ml b/ide/coqide/coqOps.ml
index 29ea3ce9ea..29ea3ce9ea 100644
--- a/ide/coqOps.ml
+++ b/ide/coqide/coqOps.ml
diff --git a/ide/coqOps.mli b/ide/coqide/coqOps.mli
index 3a4678ae9c..3a4678ae9c 100644
--- a/ide/coqOps.mli
+++ b/ide/coqide/coqOps.mli
diff --git a/ide/coq_commands.ml b/ide/coqide/coq_commands.ml
index 711986c2b2..711986c2b2 100644
--- a/ide/coq_commands.ml
+++ b/ide/coqide/coq_commands.ml
diff --git a/ide/coq_commands.mli b/ide/coqide/coq_commands.mli
index 4fa30bbe46..4fa30bbe46 100644
--- a/ide/coq_commands.mli
+++ b/ide/coqide/coq_commands.mli
diff --git a/ide/coqide/coq_icon.rc b/ide/coqide/coq_icon.rc
new file mode 100644
index 0000000000..3e8b8aaecc
--- /dev/null
+++ b/ide/coqide/coq_icon.rc
@@ -0,0 +1 @@
+large   ICON    ide/coqide/coq.ico
diff --git a/ide/coq_lex.mli b/ide/coqide/coq_lex.mli
index 142dd6e92c..142dd6e92c 100644
--- a/ide/coq_lex.mli
+++ b/ide/coqide/coq_lex.mli
diff --git a/ide/coq_lex.mll b/ide/coqide/coq_lex.mll
index fe9f108a94..fe9f108a94 100644
--- a/ide/coq_lex.mll
+++ b/ide/coqide/coq_lex.mll
diff --git a/ide/coq_style.xml b/ide/coqide/coq_style.xml
index 67631d3462..67631d3462 100644
--- a/ide/coq_style.xml
+++ b/ide/coqide/coq_style.xml
diff --git a/ide/coqide.ml b/ide/coqide/coqide.ml
index ab2a17798e..ab2a17798e 100644
--- a/ide/coqide.ml
+++ b/ide/coqide/coqide.ml
diff --git a/ide/coqide.mli b/ide/coqide/coqide.mli
index ac92afed1f..ac92afed1f 100644
--- a/ide/coqide.mli
+++ b/ide/coqide/coqide.mli
diff --git a/ide/coqide_QUARTZ.ml.in b/ide/coqide/coqide_QUARTZ.ml.in
index fe35906bdc..fe35906bdc 100644
--- a/ide/coqide_QUARTZ.ml.in
+++ b/ide/coqide/coqide_QUARTZ.ml.in
diff --git a/ide/coqide_WIN32.ml.in b/ide/coqide/coqide_WIN32.ml.in
index be8aab9e49..be8aab9e49 100644
--- a/ide/coqide_WIN32.ml.in
+++ b/ide/coqide/coqide_WIN32.ml.in
diff --git a/ide/coqide_X11.ml.in b/ide/coqide/coqide_X11.ml.in
index 76cd880ddc..76cd880ddc 100644
--- a/ide/coqide_X11.ml.in
+++ b/ide/coqide/coqide_X11.ml.in
diff --git a/ide/coqide_main.ml b/ide/coqide/coqide_main.ml
index 0812e00960..0812e00960 100644
--- a/ide/coqide_main.ml
+++ b/ide/coqide/coqide_main.ml
diff --git a/ide/coqide_main.mli b/ide/coqide/coqide_main.mli
index eeb4eb64bd..eeb4eb64bd 100644
--- a/ide/coqide_main.mli
+++ b/ide/coqide/coqide_main.mli
diff --git a/ide/coqide_os_specific.mli b/ide/coqide/coqide_os_specific.mli
index b86800dd50..b86800dd50 100644
--- a/ide/coqide_os_specific.mli
+++ b/ide/coqide/coqide_os_specific.mli
diff --git a/ide/coqide_ui.ml b/ide/coqide/coqide_ui.ml
index e9ff1bbba1..e9ff1bbba1 100644
--- a/ide/coqide_ui.ml
+++ b/ide/coqide/coqide_ui.ml
diff --git a/ide/coqide_ui.mli b/ide/coqide/coqide_ui.mli
index 9e4606072d..9e4606072d 100644
--- a/ide/coqide_ui.mli
+++ b/ide/coqide/coqide_ui.mli
diff --git a/ide/default_bindings_src.ml b/ide/coqide/default_bindings_src.ml
index a69a7c2aba..a69a7c2aba 100644
--- a/ide/default_bindings_src.ml
+++ b/ide/coqide/default_bindings_src.ml
diff --git a/ide/document.ml b/ide/coqide/document.ml
index 096c4940fa..096c4940fa 100644
--- a/ide/document.ml
+++ b/ide/coqide/document.ml
diff --git a/ide/document.mli b/ide/coqide/document.mli
index b7f23115f6..b7f23115f6 100644
--- a/ide/document.mli
+++ b/ide/coqide/document.mli
diff --git a/ide/dune b/ide/coqide/dune
index 12bad7ebc4..12bad7ebc4 100644
--- a/ide/dune
+++ b/ide/coqide/dune
diff --git a/ide/fake_ide.ml b/ide/coqide/fake_ide.ml
index e1736a5fe0..e1736a5fe0 100644
--- a/ide/fake_ide.ml
+++ b/ide/coqide/fake_ide.ml
diff --git a/ide/fileOps.ml b/ide/coqide/fileOps.ml
index 0ac14167e5..0ac14167e5 100644
--- a/ide/fileOps.ml
+++ b/ide/coqide/fileOps.ml
diff --git a/ide/fileOps.mli b/ide/coqide/fileOps.mli
index cf8084af5c..cf8084af5c 100644
--- a/ide/fileOps.mli
+++ b/ide/coqide/fileOps.mli
diff --git a/ide/gtk_parsing.ml b/ide/coqide/gtk_parsing.ml
index decd24d407..decd24d407 100644
--- a/ide/gtk_parsing.ml
+++ b/ide/coqide/gtk_parsing.ml
diff --git a/ide/gtk_parsing.mli b/ide/coqide/gtk_parsing.mli
index 501afde8ac..501afde8ac 100644
--- a/ide/gtk_parsing.mli
+++ b/ide/coqide/gtk_parsing.mli
diff --git a/ide/ide.mllib b/ide/coqide/ide.mllib
index f8e8ff48d6..f8e8ff48d6 100644
--- a/ide/ide.mllib
+++ b/ide/coqide/ide.mllib
diff --git a/ide/ide_common.mllib b/ide/coqide/ide_common.mllib
index 050c282ef6..050c282ef6 100644
--- a/ide/ide_common.mllib
+++ b/ide/coqide/ide_common.mllib
diff --git a/ide/ide_win32_stubs.c b/ide/coqide/ide_win32_stubs.c
index f430c9f2b6..f430c9f2b6 100644
--- a/ide/ide_win32_stubs.c
+++ b/ide/coqide/ide_win32_stubs.c
diff --git a/ide/idetop.ml b/ide/coqide/idetop.ml
index bd99cbed1b..bd99cbed1b 100644
--- a/ide/idetop.ml
+++ b/ide/coqide/idetop.ml
diff --git a/ide/ideutils.ml b/ide/coqide/ideutils.ml
index 482cecc1f8..482cecc1f8 100644
--- a/ide/ideutils.ml
+++ b/ide/coqide/ideutils.ml
diff --git a/ide/ideutils.mli b/ide/coqide/ideutils.mli
index 9a17eb1402..9a17eb1402 100644
--- a/ide/ideutils.mli
+++ b/ide/coqide/ideutils.mli
diff --git a/ide/macos_prehook.ml b/ide/coqide/macos_prehook.ml
index dc8fd0e85d..dc8fd0e85d 100644
--- a/ide/macos_prehook.ml
+++ b/ide/coqide/macos_prehook.ml
diff --git a/ide/macos_prehook.mli b/ide/coqide/macos_prehook.mli
index eeb4eb64bd..eeb4eb64bd 100644
--- a/ide/macos_prehook.mli
+++ b/ide/coqide/macos_prehook.mli
diff --git a/ide/microPG.ml b/ide/coqide/microPG.ml
index 5a4871b70a..5a4871b70a 100644
--- a/ide/microPG.ml
+++ b/ide/coqide/microPG.ml
diff --git a/ide/microPG.mli b/ide/coqide/microPG.mli
index f79a52f0ef..f79a52f0ef 100644
--- a/ide/microPG.mli
+++ b/ide/coqide/microPG.mli
diff --git a/ide/minilib.ml b/ide/coqide/minilib.ml
index cb7a590bd6..cb7a590bd6 100644
--- a/ide/minilib.ml
+++ b/ide/coqide/minilib.ml
diff --git a/ide/minilib.mli b/ide/coqide/minilib.mli
index 1c3be00817..1c3be00817 100644
--- a/ide/minilib.mli
+++ b/ide/coqide/minilib.mli
diff --git a/ide/preferences.ml b/ide/coqide/preferences.ml
index 5a77f4ebcf..5a77f4ebcf 100644
--- a/ide/preferences.ml
+++ b/ide/coqide/preferences.ml
diff --git a/ide/preferences.mli b/ide/coqide/preferences.mli
index 895d7a7876..895d7a7876 100644
--- a/ide/preferences.mli
+++ b/ide/coqide/preferences.mli
diff --git a/ide/protocol/dune b/ide/coqide/protocol/dune
index 801ceb20ec..801ceb20ec 100644
--- a/ide/protocol/dune
+++ b/ide/coqide/protocol/dune
diff --git a/ide/protocol/ideprotocol.mllib b/ide/coqide/protocol/ideprotocol.mllib
index 8317a08681..8317a08681 100644
--- a/ide/protocol/ideprotocol.mllib
+++ b/ide/coqide/protocol/ideprotocol.mllib
diff --git a/ide/protocol/interface.ml b/ide/coqide/protocol/interface.ml
index 646012dcaa..646012dcaa 100644
--- a/ide/protocol/interface.ml
+++ b/ide/coqide/protocol/interface.ml
diff --git a/ide/protocol/richpp.ml b/ide/coqide/protocol/richpp.ml
index 7aa38792fc..7aa38792fc 100644
--- a/ide/protocol/richpp.ml
+++ b/ide/coqide/protocol/richpp.ml
diff --git a/ide/protocol/richpp.mli b/ide/coqide/protocol/richpp.mli
index 3b83e7b15c..3b83e7b15c 100644
--- a/ide/protocol/richpp.mli
+++ b/ide/coqide/protocol/richpp.mli
diff --git a/ide/protocol/serialize.ml b/ide/coqide/protocol/serialize.ml
index bdbec5b30f..bdbec5b30f 100644
--- a/ide/protocol/serialize.ml
+++ b/ide/coqide/protocol/serialize.ml
diff --git a/ide/protocol/serialize.mli b/ide/coqide/protocol/serialize.mli
index 5d88defe55..5d88defe55 100644
--- a/ide/protocol/serialize.mli
+++ b/ide/coqide/protocol/serialize.mli
diff --git a/ide/protocol/xml_lexer.mli b/ide/coqide/protocol/xml_lexer.mli
index 920de9f9c3..920de9f9c3 100644
--- a/ide/protocol/xml_lexer.mli
+++ b/ide/coqide/protocol/xml_lexer.mli
diff --git a/ide/protocol/xml_lexer.mll b/ide/coqide/protocol/xml_lexer.mll
index e8bf7e16ae..e8bf7e16ae 100644
--- a/ide/protocol/xml_lexer.mll
+++ b/ide/coqide/protocol/xml_lexer.mll
diff --git a/ide/protocol/xml_parser.ml b/ide/coqide/protocol/xml_parser.ml
index 8db3f9e8ba..8db3f9e8ba 100644
--- a/ide/protocol/xml_parser.ml
+++ b/ide/coqide/protocol/xml_parser.ml
diff --git a/ide/protocol/xml_parser.mli b/ide/coqide/protocol/xml_parser.mli
index ac2eab352f..ac2eab352f 100644
--- a/ide/protocol/xml_parser.mli
+++ b/ide/coqide/protocol/xml_parser.mli
diff --git a/ide/protocol/xml_printer.ml b/ide/coqide/protocol/xml_printer.ml
index f526618a6e..f526618a6e 100644
--- a/ide/protocol/xml_printer.ml
+++ b/ide/coqide/protocol/xml_printer.ml
diff --git a/ide/protocol/xml_printer.mli b/ide/coqide/protocol/xml_printer.mli
index e60e3392ed..e60e3392ed 100644
--- a/ide/protocol/xml_printer.mli
+++ b/ide/coqide/protocol/xml_printer.mli
diff --git a/ide/protocol/xmlprotocol.ml b/ide/coqide/protocol/xmlprotocol.ml
index 6cb0cec008..6cb0cec008 100644
--- a/ide/protocol/xmlprotocol.ml
+++ b/ide/coqide/protocol/xmlprotocol.ml
diff --git a/ide/protocol/xmlprotocol.mli b/ide/coqide/protocol/xmlprotocol.mli
index 44584d44d7..44584d44d7 100644
--- a/ide/protocol/xmlprotocol.mli
+++ b/ide/coqide/protocol/xmlprotocol.mli
diff --git a/ide/sentence.ml b/ide/coqide/sentence.ml
index 2e00342473..2e00342473 100644
--- a/ide/sentence.ml
+++ b/ide/coqide/sentence.ml
diff --git a/ide/sentence.mli b/ide/coqide/sentence.mli
index adaa7c5d2f..adaa7c5d2f 100644
--- a/ide/sentence.mli
+++ b/ide/coqide/sentence.mli
diff --git a/ide/session.ml b/ide/coqide/session.ml
index 09391b7f50..09391b7f50 100644
--- a/ide/session.ml
+++ b/ide/coqide/session.ml
diff --git a/ide/session.mli b/ide/coqide/session.mli
index 9c0a8760c3..9c0a8760c3 100644
--- a/ide/session.mli
+++ b/ide/coqide/session.mli
diff --git a/ide/tags.ml b/ide/coqide/tags.ml
index 82e63e84a5..82e63e84a5 100644
--- a/ide/tags.ml
+++ b/ide/coqide/tags.ml
diff --git a/ide/tags.mli b/ide/coqide/tags.mli
index 61109c6d60..61109c6d60 100644
--- a/ide/tags.mli
+++ b/ide/coqide/tags.mli
diff --git a/ide/unicode_bindings.ml b/ide/coqide/unicode_bindings.ml
index 39d58825df..39d58825df 100644
--- a/ide/unicode_bindings.ml
+++ b/ide/coqide/unicode_bindings.ml
diff --git a/ide/unicode_bindings.mli b/ide/coqide/unicode_bindings.mli
index 30c6d91fa0..30c6d91fa0 100644
--- a/ide/unicode_bindings.mli
+++ b/ide/coqide/unicode_bindings.mli
diff --git a/ide/utf8_convert.mli b/ide/coqide/utf8_convert.mli
index f1d8aedecb..f1d8aedecb 100644
--- a/ide/utf8_convert.mli
+++ b/ide/coqide/utf8_convert.mli
diff --git a/ide/utf8_convert.mll b/ide/coqide/utf8_convert.mll
index db02bd8116..db02bd8116 100644
--- a/ide/utf8_convert.mll
+++ b/ide/coqide/utf8_convert.mll
diff --git a/ide/wg_Command.ml b/ide/coqide/wg_Command.ml
index 30924adc4a..30924adc4a 100644
--- a/ide/wg_Command.ml
+++ b/ide/coqide/wg_Command.ml
diff --git a/ide/wg_Command.mli b/ide/coqide/wg_Command.mli
index e2854cc6d5..e2854cc6d5 100644
--- a/ide/wg_Command.mli
+++ b/ide/coqide/wg_Command.mli
diff --git a/ide/wg_Completion.ml b/ide/coqide/wg_Completion.ml
index cc24e71386..cc24e71386 100644
--- a/ide/wg_Completion.ml
+++ b/ide/coqide/wg_Completion.ml
diff --git a/ide/wg_Completion.mli b/ide/coqide/wg_Completion.mli
index 8bb34fbbca..8bb34fbbca 100644
--- a/ide/wg_Completion.mli
+++ b/ide/coqide/wg_Completion.mli
diff --git a/ide/wg_Detachable.ml b/ide/coqide/wg_Detachable.ml
index efb10293bd..efb10293bd 100644
--- a/ide/wg_Detachable.ml
+++ b/ide/coqide/wg_Detachable.ml
diff --git a/ide/wg_Detachable.mli b/ide/coqide/wg_Detachable.mli
index 09b4ac732d..09b4ac732d 100644
--- a/ide/wg_Detachable.mli
+++ b/ide/coqide/wg_Detachable.mli
diff --git a/ide/wg_Find.ml b/ide/coqide/wg_Find.ml
index 7e89191bd1..7e89191bd1 100644
--- a/ide/wg_Find.ml
+++ b/ide/coqide/wg_Find.ml
diff --git a/ide/wg_Find.mli b/ide/coqide/wg_Find.mli
index 2a26230a6a..2a26230a6a 100644
--- a/ide/wg_Find.mli
+++ b/ide/coqide/wg_Find.mli
diff --git a/ide/wg_MessageView.ml b/ide/coqide/wg_MessageView.ml
index 6e22172d05..6e22172d05 100644
--- a/ide/wg_MessageView.ml
+++ b/ide/coqide/wg_MessageView.ml
diff --git a/ide/wg_MessageView.mli b/ide/coqide/wg_MessageView.mli
index 054dd0e571..054dd0e571 100644
--- a/ide/wg_MessageView.mli
+++ b/ide/coqide/wg_MessageView.mli
diff --git a/ide/wg_Notebook.ml b/ide/coqide/wg_Notebook.ml
index 9662880210..9662880210 100644
--- a/ide/wg_Notebook.ml
+++ b/ide/coqide/wg_Notebook.ml
diff --git a/ide/wg_Notebook.mli b/ide/coqide/wg_Notebook.mli
index d3907f43ad..d3907f43ad 100644
--- a/ide/wg_Notebook.mli
+++ b/ide/coqide/wg_Notebook.mli
diff --git a/ide/wg_ProofView.ml b/ide/coqide/wg_ProofView.ml
index 1de63953af..1de63953af 100644
--- a/ide/wg_ProofView.ml
+++ b/ide/coqide/wg_ProofView.ml
diff --git a/ide/wg_ProofView.mli b/ide/coqide/wg_ProofView.mli
index 8217f72066..8217f72066 100644
--- a/ide/wg_ProofView.mli
+++ b/ide/coqide/wg_ProofView.mli
diff --git a/ide/wg_RoutedMessageViews.ml b/ide/coqide/wg_RoutedMessageViews.ml
index f141343c5d..f141343c5d 100644
--- a/ide/wg_RoutedMessageViews.ml
+++ b/ide/coqide/wg_RoutedMessageViews.ml
diff --git a/ide/wg_RoutedMessageViews.mli b/ide/coqide/wg_RoutedMessageViews.mli
index bf9893852a..bf9893852a 100644
--- a/ide/wg_RoutedMessageViews.mli
+++ b/ide/coqide/wg_RoutedMessageViews.mli
diff --git a/ide/wg_ScriptView.ml b/ide/coqide/wg_ScriptView.ml
index 62d58a5f23..62d58a5f23 100644
--- a/ide/wg_ScriptView.ml
+++ b/ide/coqide/wg_ScriptView.ml
diff --git a/ide/wg_ScriptView.mli b/ide/coqide/wg_ScriptView.mli
index 849c308941..849c308941 100644
--- a/ide/wg_ScriptView.mli
+++ b/ide/coqide/wg_ScriptView.mli
diff --git a/ide/wg_Segment.ml b/ide/coqide/wg_Segment.ml
index f115da662e..f115da662e 100644
--- a/ide/wg_Segment.ml
+++ b/ide/coqide/wg_Segment.ml
diff --git a/ide/wg_Segment.mli b/ide/coqide/wg_Segment.mli
index 9464b596e5..9464b596e5 100644
--- a/ide/wg_Segment.mli
+++ b/ide/coqide/wg_Segment.mli