Imported Upstream version 8.9.0upstream/8.9.0upstream

17 files changed, 93 insertions, 2110 deletions

diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in
index f7e30eae..403ad617 100644
--- a/tools/CoqMakefile.in
+++ b/tools/CoqMakefile.in
@@ -86,7 +86,6 @@ COQC     ?= "$(COQBIN)coqc"
 COQTOP   ?= "$(COQBIN)coqtop"
 COQCHK   ?= "$(COQBIN)coqchk"
 COQDEP   ?= "$(COQBIN)coqdep"
-GALLINA  ?= "$(COQBIN)gallina"
 COQDOC   ?= "$(COQBIN)coqdoc"
 COQMKFILE ?= "$(COQBIN)coq_makefile"
 
@@ -148,7 +147,11 @@ TIME_OF_PRETTY_BUILD_EXTRA_FILES ?= - # also output to the command line
 
 # Flags #######################################################################
 #
-# We define a bunch of variables combining the parameters
+# We define a bunch of variables combining the parameters.
+# To add additional flags to coq, coqchk or coqdoc, set the
+# {COQ,COQCHK,COQDOC}EXTRAFLAGS variable to whatever you want to add.
+# To overwrite the default choice and set your own flags entirely, set the
+# {COQ,COQCHK,COQDOC}FLAGS variable.
 
 SHOW := $(if $(VERBOSE),@true "",@echo "")
 HIDE := $(if $(VERBOSE),,@)
@@ -168,9 +171,16 @@ DYNOBJ:=.cmxs
 DYNLIB:=.cmxs
 endif
 
-COQFLAGS?=-q $(OPT) $(COQLIBS) $(OTHERFLAGS)
-COQCHKFLAGS?=-silent -o $(COQLIBS)
-COQDOCFLAGS?=-interpolate -utf8
+# these variables are meant to be overriden if you want to add *extra* flags
+COQEXTRAFLAGS?=
+COQCHKEXTRAFLAGS?=
+COQDOCEXTRAFLAGS?=
+
+# these flags do NOT contain the libraries, to make them easier to overwrite
+COQFLAGS?=-q $(OPT) $(OTHERFLAGS) $(COQEXTRAFLAGS)
+COQCHKFLAGS?=-silent -o $(COQCHKEXTRAFLAGS)
+COQDOCFLAGS?=-interpolate -utf8 $(COQDOCEXTRAFLAGS)
+
 COQDOCLIBS?=$(COQLIBS_NOML)
 
 # The version of Coq being run and the version of coq_makefile that
@@ -245,7 +255,6 @@ VO = vo
 
 VOFILES = $(VFILES:.v=.$(VO))
 GLOBFILES = $(VFILES:.v=.glob)
-GFILES = $(VFILES:.v=.g)
 HTMLFILES = $(VFILES:.v=.html)
 GHTMLFILES = $(VFILES:.v=.g.html)
 BEAUTYFILES = $(addsuffix .beautified,$(VFILES))
@@ -384,7 +393,7 @@ quick: $(VOFILES:.vo=.vio)
 .PHONY: quick
 
 vio2vo:
-	$(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) \
+	$(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) \
 		-schedule-vio2vo $(J) $(VOFILES:%.vo=%.vio)
 .PHONY: vio2vo
 
@@ -396,17 +405,17 @@ quick2vo:
 	done); \
 	echo "VIO2VO: $$VIOFILES"; \
 	if [ -n "$$VIOFILES" ]; then \
-	  $(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) -schedule-vio2vo $(J) $$VIOFILES; \
+	  $(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) -schedule-vio2vo $(J) $$VIOFILES; \
 	fi
 .PHONY: quick2vo
 
 checkproofs:
-	$(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) \
+	$(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) \
 		-schedule-vio-checking $(J) $(VOFILES:%.vo=%.vio)
 .PHONY: checkproofs
 
 validate: $(VOFILES)
-	$(TIMER) $(COQCHK) $(COQCHKFLAGS) $^
+	$(TIMER) $(COQCHK) $(COQCHKFLAGS) $(COQLIBS) $^
 .PHONY: validate
 
 only: $(TGTS)
@@ -431,8 +440,6 @@ all-mli.tex: $(MLIFILES:.mli=.cmi)
 	$(HIDE)$(CAMLDOC) -latex \
 		-o $@ -m A $(CAMLDEBUG) $(CAMLDOCFLAGS) $(MLIFILES)
 
-gallina: $(GFILES)
-
 all.ps: $(VFILES)
 	$(SHOW)'COQDOC -ps $(GAL)'
 	$(HIDE)$(COQDOC) \
@@ -553,7 +560,6 @@ clean::
 	$(HIDE)find . -name .coq-native -type d -empty -delete
 	$(HIDE)rm -f $(VOFILES)
 	$(HIDE)rm -f $(VOFILES:.vo=.vio)
-	$(HIDE)rm -f $(GFILES)
 	$(HIDE)rm -f $(BEAUTYFILES) $(VFILES:=.old)
 	$(HIDE)rm -f all.ps all-gal.ps all.pdf all-gal.pdf all.glob all-mli.tex
 	$(HIDE)rm -f $(VFILES:.v=.glob)
@@ -654,15 +660,15 @@ endif
 
 $(VOFILES): %.vo: %.v
 	$(SHOW)COQC $<
-	$(HIDE)$(TIMER) $(COQC) $(COQDEBUG) $(TIMING_ARG) $(COQFLAGS) $< $(TIMING_EXTRA)
+	$(HIDE)$(TIMER) $(COQC) $(COQDEBUG) $(TIMING_ARG) $(COQFLAGS) $(COQLIBS) $< $(TIMING_EXTRA)
 
 # FIXME ?merge with .vo / .vio ?
 $(GLOBFILES): %.glob: %.v
-	$(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $<
+	$(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $<
 
 $(VFILES:.v=.vio): %.vio: %.v
 	$(SHOW)COQC -quick $<
-	$(HIDE)$(TIMER) $(COQC) -quick $(COQDEBUG) $(COQFLAGS) $<
+	$(HIDE)$(TIMER) $(COQC) -quick $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $<
 
 $(addsuffix .timing.diff,$(VFILES)): %.timing.diff : %.before-timing %.after-timing
 	$(SHOW)PYTHON TIMING-DIFF $<
@@ -670,11 +676,7 @@ $(addsuffix .timing.diff,$(VFILES)): %.timing.diff : %.before-timing %.after-tim
 
 $(BEAUTYFILES): %.v.beautified: %.v
 	$(SHOW)'BEAUTIFY $<'
-	$(HIDE)$(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) -beautify $<
-
-$(GFILES): %.g: %.v
-	$(SHOW)'GALLINA $<'
-	$(HIDE)$(GALLINA) $<
+	$(HIDE)$(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) -beautify $<
 
 $(TEXFILES): %.tex: %.v
 	$(SHOW)'COQDOC -latex $<'
@@ -764,6 +766,7 @@ printenv::
 	@echo 'OCAMLFIND = $(OCAMLFIND)'
 	@echo 'PP = $(PP)'
 	@echo 'COQFLAGS = $(COQFLAGS)'
+	@echo 'COQLIB = $(COQLIBS)'
 	@echo 'COQLIBINSTALL = $(COQLIBINSTALL)'
 	@echo 'COQDOCINSTALL = $(COQDOCINSTALL)'
 .PHONY:	printenv
diff --git a/tools/coq-font-lock.el b/tools/coq-font-lock.el
deleted file mode 100644
index 068e6400..00000000
--- a/tools/coq-font-lock.el
+++ /dev/null
@@ -1,137 +0,0 @@
-;; coq-font-lock.el --- Coq syntax highlighting for Emacs - compatibilty code
-;; Pierre Courtieu, may 2009
-;;
-;; Authors: Pierre Courtieu
-;; License:     GPL (GNU GENERAL PUBLIC LICENSE)
-;; Maintainer: Pierre Courtieu <Pierre.Courtieu@cnam.fr>
-
-;; This is copy paste from ProofGeneral by David Aspinall
-;; <David.Aspinall@ed.ac.uk>. ProofGeneral is under GPL and Copyright
-;; (C) LFCS Edinburgh.
-
-
-;;; Commentary:
-;; This file contains the code necessary to coq-syntax.el and
-;; coq-db.el from ProofGeneral. It is also pocked from ProofGeneral.
-
-
-;;; History:
-;; First created from ProofGeneral may 28th 2009
-
-
-;;; Code:
-
-(setq coq-version-is-V8-1 t)
-(defun coq-build-regexp-list-from-db (db &optional filter)
-  "Take a keyword database DB and return the list of regexps for font-lock.
-If non-nil Optional argument FILTER is a function applying to each line of DB.
-For each line if FILTER returns nil, then the keyword is not added to the
-regexp.  See `coq-syntax-db' for DB structure."
-  (let ((l db) (res ()))
-    (while l
-      (let* ((hd (car l)) (tl (cdr l))	; hd is the first infos list
-             (e1 (car hd)) (tl1 (cdr hd)) ; e1 = menu entry
-             (e2 (car tl1)) (tl2 (cdr tl1)) ; e2 = abbreviation
-             (e3 (car tl2)) (tl3 (cdr tl2)) ; e3 = completion
-             (e4 (car-safe tl3)) (tl4 (cdr-safe tl3)) ; e4 = state changing
-             (e5 (car-safe tl4)) (tl5 (cdr-safe tl4)) ; e5 = colorization string
-             )
-        ;; TODO delete doublons
-        (when (and e5 (or (not filter) (funcall filter hd)))
-          (setq res (nconc res (list e5)))) ; careful: nconc destructive!
-        (setq l tl)))
-    res
-    ))
-(defun filter-state-preserving (l)
-  ; checkdoc-params: (l)
-  "Not documented."
-  (not (nth 3 l))) ; fourth argument is nil --> state preserving command
-
-(defun filter-state-changing (l)
-  ; checkdoc-params: (l)
-  "Not documented."
-  (nth 3 l)) ; fourth argument is nil --> state preserving command
-
-;; Generic font-lock
-
-(defvar proof-id "\\(\\w\\(\\w\\|\\s_\\)*\\)"
-  "A regular expression for parsing identifiers.")
-
-;; For font-lock, we treat ,-separated identifiers as one identifier
-;; and refontify commata using \{proof-zap-commas}.
-
-(defun proof-anchor-regexp (e)
-  "Anchor (\\`) and group the regexp E."
-  (concat "\\`\\(" e "\\)"))
-
-(defun proof-ids (proof-id &optional sepregexp)
-  "Generate a regular expression for separated lists of identifiers PROOF-ID.
-Default is comma separated, or SEPREGEXP if set."
-  (concat proof-id "\\(\\s-*"   (or sepregexp ",") "\\s-*"
-	  proof-id "\\)*"))
-
-(defun proof-ids-to-regexp (l)
-  "Maps a non-empty list of tokens `L' to a regexp matching any element."
-  (if (featurep 'xemacs)
-      (mapconcat (lambda (s) (concat "\\_<" s "\\_>")) l "\\|") ;; old version
-    (concat "\\_<\\(?:" (mapconcat 'identity l "\\|") "\\)\\_>")))
-
-;; TODO: get rid of this list.  Does 'default work widely enough
-;; by now?
-(defconst pg-defface-window-systems
-  '(x            ;; bog standard
-    mswindows    ;; Windows
-    w32	         ;; Windows
-    gtk          ;; gtk emacs (obsolete?)
-    mac          ;; used by Aquamacs
-    carbon       ;; used by Carbon XEmacs
-    ns           ;; NeXTstep Emacs (Emacs.app)
-    x-toolkit)   ;; possible catch all (but probably not)
-  "A list of possible values for variable `window-system'.
-If you are on a window system and your value of variable
-`window-system' is not listed here, you may not get the correct
-syntax colouring behaviour.")
-
-(defmacro proof-face-specs (bl bd ow)
-  "Return a spec for `defface' with BL for light bg, BD for dark, OW o/w."
-  `(append
-    (apply 'append
-     (mapcar
-     (lambda (ty) (list
-		     (list (list (list 'type ty) '(class color)
-			   (list 'background 'light))
-			   (quote ,bl))
-		     (list (list (list 'type ty) '(class color)
-				 (list 'background 'dark))
-			   (quote ,bd))))
-     pg-defface-window-systems))
-    (list (list t (quote ,ow)))))
-
-;;A new face for tactics
-(defface coq-solve-tactics-face
-  (proof-face-specs
-   (:foreground "forestgreen" t) ; for bright backgrounds
-   (:foreground "forestgreen"  t) ; for dark backgrounds
-   ()) ; for black and white
-  "Face for names of closing tactics in proof scripts."
-  :group 'proof-faces)
-
-;;A new face for tactics which fail when they don't kill the current goal
-(defface coq-solve-tactics-face
-  (proof-face-specs
-   (:foreground "red" t) ; for bright backgrounds
-   (:foreground "red"  t) ; for dark backgrounds
-   ()) ; for black and white
-  "Face for names of closing tactics in proof scripts."
-  :group 'proof-faces)
-
-
-(defconst coq-solve-tactics-face 'coq-solve-tactics-face
-  "Expression that evaluates to a face.
-Required so that 'proof-solve-tactics-face is a proper facename")
-
-(defconst proof-tactics-name-face 'coq-solve-tactics-face)
-(defconst proof-tacticals-name-face 'coq-solve-tactics-face)
-
-(provide 'coq-font-lock)
-;;; coq-font-lock.el ends here
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index 5402765f..0e56cc3c 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -59,7 +59,7 @@ let usage_coq_makefile () =
 \n _-extra-phony foo bar \"\"_ is a regular way to add the target \"bar\" as\
 \n as a dependencies of an already defined target \"foo\".\
 \n[-I dir]: look for Objective Caml dependencies in \"dir\"\
-\n[-R physicalpath logicalpath]: look for Coq dependencies resursively\
+\n[-R physicalpath logicalpath]: look for Coq dependencies recursively\
 \n  starting from \"physicalpath\". The logical path associated to the\
 \n  physical path is \"logicalpath\".\
 \n[-Q physicalpath logicalpath]: look for Coq dependencies starting from\
@@ -210,7 +210,7 @@ let windrive s =
   else ""
 ;;
 
-let generate_conf_coq_config oc args =
+let generate_conf_coq_config oc =
   section oc "Coq configuration.";
   let src_dirs = Coq_config.all_src_dirs in
   Envars.print_config ~prefix_var_name:"COQMF_" oc src_dirs;
@@ -274,7 +274,7 @@ let generate_conf oc project args  =
   fprintf oc "# %s\n\n" (String.concat " " (List.map quote args));
   generate_conf_files oc project;
   generate_conf_includes oc project;
-  generate_conf_coq_config oc args;
+  generate_conf_coq_config oc;
   generate_conf_defs oc project;
   generate_conf_doc oc project;
   generate_conf_extra_target oc project.extra_targets;
diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index 12b5cab0..7db0b289 100644
--- a/tools/coqdep.ml
+++ b/tools/coqdep.ml
@@ -8,15 +8,24 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-open Printf
+open Format
 open Coqdep_lexer
 open Coqdep_common
-open System
+open Minisys
 
 (** The basic parts of coqdep (i.e. the parts used by [coqdep -boot])
     are now in [Coqdep_common]. The code that remains here concerns
     the other options. Calling this complete coqdep with the [-boot]
     option should be equivalent to calling [coqdep_boot].
+
+    As of today, this module depends on the following Coq modules:
+
+    - Flags
+    - Envars
+    - CoqProject_file
+
+    All of it for `coqlib` handling. Ideally we would like to clean
+    coqlib handling up so this can be bootstrapped earlier.
 *)
 
 let option_D = ref false
@@ -31,8 +40,7 @@ let warning_mult suf iter =
       let d' = Hashtbl.find tab f in
       if (Filename.dirname (file_name f d))
         <> (Filename.dirname (file_name f d')) then begin
-	  eprintf "*** Warning : the file %s is defined twice!\n" (f ^ suf);
-	  flush stderr
+          coqdep_warning "the file %s is defined twice!" (f ^ suf)
 	end
     with Not_found -> () end;
     Hashtbl.add tab f d
@@ -80,9 +88,7 @@ let mL_dep_list b f =
 	while true do
 	  let (Use_module str) = caml_action buf in
 	  if str = b then begin
-	    eprintf "*** Warning : in file %s the" f;
-	    eprintf " notation %s. is useless !\n" b;
-	    flush stderr
+            coqdep_warning "in file %s the notation %s. is useless !\n" f b
 	  end else
             if not (List.mem str !deja_vu) then addQueue deja_vu str
       	done; []
@@ -98,16 +104,13 @@ let affiche_Declare f dcl =
   printf "\n*** In file %s: \n" f;
   printf "Declare ML Module";
   List.iter (fun str -> printf " \"%s\"" str) dcl;
-  printf ".\n";
-  flush stdout
+  printf ".\n%!"
 
 let warning_Declare f dcl =
-  eprintf "*** Warning : in file %s, the ML modules" f;
-  eprintf " declaration should be\n";
+  eprintf "*** Warning : in file %s, the ML modules declaration should be\n" f;
   eprintf "*** Declare ML Module";
   List.iter (fun str -> eprintf " \"%s\"" str) dcl;
-  eprintf ".\n";
-  flush stderr
+  eprintf ".\n%!"
 
 let traite_Declare f =
   let decl_list = ref ([] : string list) in
@@ -149,7 +152,7 @@ let declare_dependencies () =
   List.iter
     (fun (name,_) ->
        traite_Declare (name^".v");
-       flush stdout)
+       pp_print_flush std_formatter ())
     (List.rev !vAccu)
 
 (** DAGs guaranteed to be transitive reductions *)
@@ -426,11 +429,11 @@ let coq_dependencies_dump chan dumpboxes =
     (DAG.empty, List.fold_left (fun ih (file, _) -> insert_raw_graph file ih) [] !vAccu,
     List.map fst !vAccu) !vAccu
   in
-  fprintf chan "digraph dependencies {\n"; flush chan;
+  fprintf chan "digraph dependencies {\n";
   if dumpboxes then print_graphs chan (pop_common_prefix graphs)
   else List.iter (fun (name, _) -> fprintf chan "\"%s\"[label=\"%s\"]\n" name (basename_noext name)) !vAccu;
   DAG.iter (fun name dep -> fprintf chan "\"%s\" -> \"%s\"\n" dep name) deps;
-  fprintf chan "}\n"
+  fprintf chan "}\n%!"
 
 end
 
@@ -498,7 +501,7 @@ let rec parse = function
   | "-suffix" :: s :: ll -> suffixe := s ; parse ll
   | "-suffix" :: [] -> usage ()
   | "-slash" :: ll ->
-    Printf.eprintf "warning: option -slash has no effect and is deprecated.\n";
+    coqdep_warning "warning: option -slash has no effect and is deprecated.";
     parse ll
   | "-dyndep" :: "no" :: ll -> option_dynlink := No; parse ll
   | "-dyndep" :: "opt" :: ll -> option_dynlink := Opt; parse ll
@@ -509,6 +512,9 @@ let rec parse = function
   | f :: ll -> treat_file None f; parse ll
   | [] -> ()
 
+(* Exception to be raised by Envars *)
+exception CoqlibError of string
+
 let coqdep () =
   if Array.length Sys.argv < 2 then usage ();
   if not Coq_config.has_natdynlink then option_dynlink := No;
@@ -520,18 +526,17 @@ let coqdep () =
   if !option_boot then begin
     add_rec_dir_import add_known "theories" ["Coq"];
     add_rec_dir_import add_known "plugins" ["Coq"];
-    add_caml_dir "tactics";
     add_rec_dir_import (fun _ -> add_caml_known) "theories" ["Coq"];
     add_rec_dir_import (fun _ -> add_caml_known) "plugins" ["Coq"];
   end else begin
-    Envars.set_coqlib ~fail:(fun msg -> CErrors.user_err Pp.(str msg));
+    Envars.set_coqlib ~fail:(fun msg -> raise (CoqlibError msg));
     let coqlib = Envars.coqlib () in
     add_rec_dir_import add_coqlib_known (coqlib//"theories") ["Coq"];
     add_rec_dir_import add_coqlib_known (coqlib//"plugins") ["Coq"];
     let user = coqlib//"user-contrib" in
     if Sys.file_exists user then add_rec_dir_no_import add_coqlib_known user [];
     List.iter (fun s -> add_rec_dir_no_import add_coqlib_known s [])
-      (Envars.xdg_dirs ~warn:(fun x -> Feedback.msg_warning (Pp.str x)));
+      (Envars.xdg_dirs ~warn:(fun x -> coqdep_warning "%s" x));
     List.iter (fun s -> add_rec_dir_no_import add_coqlib_known s []) Envars.coqpath;
   end;
   List.iter (fun (f,d) -> add_mli_known f d ".mli") !mliAccu;
@@ -547,13 +552,13 @@ let coqdep () =
   | None -> ()
   | Some (box, file) ->
     let chan = open_out file in
-    try Graph.coq_dependencies_dump chan box; close_out chan
+    let chan_fmt = formatter_of_out_channel chan in
+    try Graph.coq_dependencies_dump chan_fmt box; close_out chan
     with e -> close_out chan; raise e
   end
 
 let _ =
   try
     coqdep ()
-  with CErrors.UserError(s,p) ->
-    let pp = (match s with | None -> p | Some s -> Pp.(str s ++ str ": " ++ p))  in
-    Format.eprintf "%a@\n%!" Pp.pp_with pp
+  with CoqlibError msg ->
+    eprintf "*** Error: %s@\n%!" msg
diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml
index db69a3b7..23b8bc11 100644
--- a/tools/coqdep_common.ml
+++ b/tools/coqdep_common.ml
@@ -8,9 +8,9 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-open Printf
-open Coqdep_lexer
+open Format
 open Unix
+open Coqdep_lexer
 open Minisys
 
 (** [coqdep_boot] is a stripped-down version of [coqdep], whose
@@ -20,14 +20,15 @@ open Minisys
     options (see for instance [option_dynlink] below).
 *)
 
+let coqdep_warning args =
+  eprintf "*** Warning: @[";
+  kfprintf (fun fmt -> fprintf fmt "@]\n%!") err_formatter args
+
 module StrSet = Set.Make(String)
 
 module StrList = struct type t = string list let compare = compare end
 module StrListMap = Map.Make(StrList)
 
-let stderr = Pervasives.stderr
-let stdout = Pervasives.stdout
-
 type dynlink = Opt | Byte | Both | No | Variable
 
 let option_c = ref false
@@ -114,8 +115,7 @@ let same_path_opt s s' =
 
 let warning_ml_clash x s suff s' suff' =
   if suff = suff' && not (same_path_opt s s') then
-  eprintf
-    "*** Warning: %s%s already found in %s (discarding %s%s)\n" x suff
+  coqdep_warning "%s%s already found in %s (discarding %s%s)\n" x suff
     (match s with None -> "." | Some d -> d)
     ((match s' with None -> "." | Some d -> d) // x) suff
 
@@ -180,13 +180,11 @@ let error_cannot_parse s (i,j) =
   exit 1
 
 let warning_module_notfound f s =
-  eprintf "*** Warning: in file %s, library %s is required and has not been found in the loadpath!\n%!"
+  coqdep_warning "in file %s, library %s is required and has not been found in the loadpath!"
     f (String.concat "." s)
 
 let warning_declare f s =
-  eprintf "*** Warning: in file %s, declared ML module " f;
-  eprintf "%s has not been found!\n" s;
-  flush stderr
+  coqdep_warning "in file %s, declared ML module %s has not been found!" f s
 
 let warning_clash file dir =
   match StrListMap.find dir !clash_v with
@@ -203,8 +201,7 @@ let warning_clash file dir =
   | _ -> assert false
 
 let warning_cannot_open_dir dir =
-  eprintf "*** Warning: cannot open %s\n" dir;
-  flush stderr
+  coqdep_warning "cannot open %s" dir
 
 let safe_assoc from verbose file k =
   if verbose && StrListMap.mem k !clash_v then warning_clash file k;
@@ -451,15 +448,13 @@ let mL_dependencies () =
        in
        let efullname = escape fullname in
        printf "%s.cmo:%s%s\n" efullname dep intf;
-       printf "%s.cmx:%s%s\n" efullname dep_opt intf;
-       flush stdout)
+       printf "%s.cmx:%s%s\n%!" efullname dep_opt intf)
     (List.rev !mlAccu);
   List.iter
     (fun (name,dirname) ->
        let fullname = file_name name dirname in
        let (dep,_) = traite_fichier_ML fullname ".mli" in
-       printf "%s.cmi:%s\n" (escape fullname) dep;
-       flush stdout)
+       printf "%s.cmi:%s\n%!" (escape fullname) dep)
     (List.rev !mliAccu);
   List.iter
     (fun (name,dirname) ->
@@ -468,8 +463,7 @@ let mL_dependencies () =
        let efullname = escape fullname in
        printf "%s_MLLIB_DEPENDENCIES:=%s\n" efullname (String.concat " " dep);
        printf "%s.cma:$(addsuffix .cmo,$(%s_MLLIB_DEPENDENCIES))\n" efullname efullname;
-       printf "%s.cmxa:$(addsuffix .cmx,$(%s_MLLIB_DEPENDENCIES))\n" efullname efullname;
-       flush stdout)
+       printf "%s.cmxa:$(addsuffix .cmx,$(%s_MLLIB_DEPENDENCIES))\n%!" efullname efullname)
     (List.rev !mllibAccu);
   List.iter
     (fun (name,dirname) ->
@@ -483,7 +477,7 @@ let mL_dependencies () =
        List.iter (fun dep ->
          printf "%s.cmx : FOR_PACK=-for-pack %s\n" dep efullname_capital)
          dep;
-       flush stdout)
+       printf "%!")
     (List.rev !mlpackAccu)
 
 let coq_dependencies () =
@@ -496,8 +490,7 @@ let coq_dependencies () =
        printf "\n";
        printf "%s.vio: %s.v" ename ename;
        traite_fichier_Coq ".vio" true (name ^ ".v");
-       printf "\n";
-       flush stdout)
+       printf "\n%!")
     (List.rev !vAccu)
 
 let rec suffixes = function
diff --git a/tools/coqdep_common.mli b/tools/coqdep_common.mli
index d0d79324..91d2b458 100644
--- a/tools/coqdep_common.mli
+++ b/tools/coqdep_common.mli
@@ -10,6 +10,8 @@
 
 module StrSet : Set.S with type elt = string
 
+val coqdep_warning : ('a, Format.formatter, unit, unit) format4 -> 'a
+
 (** [find_dir_logpath dir] Return the logical path of directory [dir]
     if it has been given one. Raise [Not_found] otherwise. In
     particular we can check if "." has been attributed a logical path
diff --git a/tools/coqdoc/index.ml b/tools/coqdoc/index.ml
index df493fdf..724d3838 100644
--- a/tools/coqdoc/index.ml
+++ b/tools/coqdoc/index.ml
@@ -77,7 +77,7 @@ let add_ref m loc m' sp id ty =
 
 let find m l = Hashtbl.find reftable (m, l)
 
-let find_string m s = let (m,s,t) = Hashtbl.find byidtable s in Ref (m,s,t)
+let find_string s = let (m,s,t) = Hashtbl.find byidtable s in Ref (m,s,t)
 
 (* Coq modules *)
 
@@ -185,7 +185,8 @@ let type_name = function
 let prepare_entry s = function
   | Notation ->
       (* We decode the encoding done in Dumpglob.cook_notation of coqtop *)
-      (* Encoded notations have the form section:sc:x_'++'_x where:      *)
+      (* Encoded notations have the form section:entry:sc:x_'++'_x       *)
+      (* where:                                                          *)
       (* - the section, if any, ends with a "."                          *)
       (* - the scope can be empty                                        *)
       (* - tokens are separated with "_"                                 *)
@@ -202,10 +203,12 @@ let prepare_entry s = function
       let err () = eprintf "Invalid notation in globalization file\n"; exit 1 in
       let h = try String.index_from s 0 ':' with _ -> err () in
       let i = try String.index_from s (h+1) ':' with _ -> err () in
-      let sc = String.sub s (h+1) (i-h-1) in
-      let ntn = Bytes.make (String.length s - i) ' ' in
+      let m = try String.index_from s (i+1) ':' with _ -> err () in
+      let entry = String.sub s (h+1) (i-h-1) in
+      let sc = String.sub s (i+1) (m-i-1) in
+      let ntn = Bytes.make (String.length s - m) ' ' in
       let k = ref 0 in
-      let j = ref (i+1) in
+      let j = ref (m+1) in
       let quoted = ref false in
       let l = String.length s - 1 in
       while !j <= l do
@@ -227,7 +230,8 @@ let prepare_entry s = function
 	incr j
       done;
       let ntn = Bytes.sub_string ntn 0 !k in
-      if sc = "" then ntn else ntn ^ " (" ^ sc ^ ")"
+      let ntn = if sc = "" then ntn else ntn ^ " (" ^ sc ^ ")" in
+      if entry = "" then ntn else entry ^ ":" ^ ntn
   | _ ->
       s
 
diff --git a/tools/coqdoc/index.mli b/tools/coqdoc/index.mli
index 5cd30138..7c9aad67 100644
--- a/tools/coqdoc/index.mli
+++ b/tools/coqdoc/index.mli
@@ -41,7 +41,7 @@ type index_entry =
 val find : coq_module -> loc -> index_entry
 
 (* Find what data is referred to by some string in some coq module *)
-val find_string : coq_module -> string -> index_entry
+val find_string : string -> index_entry
 
 val add_module : coq_module -> unit
 
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml
index d2522700..750698a1 100644
--- a/tools/coqdoc/output.ml
+++ b/tools/coqdoc/output.ml
@@ -76,7 +76,7 @@ let is_tactic =
     [ "intro"; "intros"; "apply"; "rewrite"; "refine"; "case"; "clear"; "injection";
       "elimtype"; "progress"; "setoid_rewrite"; "left"; "right"; "constructor"; 
       "econstructor"; "decide equality"; "abstract"; "exists"; "cbv"; "simple destruct";
-      "info"; "fourier"; "field"; "specialize"; "evar"; "solve"; "instanciate"; "info_auto"; "info_eauto";
+      "info"; "field"; "specialize"; "evar"; "solve"; "instantiate"; "info_auto"; "info_eauto";
       "quote"; "eexact"; "autorewrite";
       "destruct"; "destruction"; "destruct_call"; "dependent"; "elim"; "extensionality";
       "f_equal"; "generalize"; "generalize_eqs"; "generalize_eqs_vars"; "induction"; "rename"; "move"; "omega";
@@ -431,7 +431,7 @@ module Latex = struct
       else if !Cdglobals.interpolate && !in_doc (* always a var otherwise *)
       then
 	try
-	  let tag = Index.find_string (get_module false) s in
+          let tag = Index.find_string s in
 	  reference (translate s) tag
 	with _ -> Tokens.output_tagged_ident_string s
       else Tokens.output_tagged_ident_string s
@@ -706,7 +706,7 @@ module Html = struct
       else if is_keyword s then
         printf "<span class=\"id\" title=\"keyword\">%s</span>" (translate s)
       else if !Cdglobals.interpolate && !in_doc (* always a var otherwise *) then
-	try reference (translate s) (Index.find_string (get_module false) s)
+        try reference (translate s) (Index.find_string s)
 	with Not_found -> Tokens.output_tagged_ident_string s
       else
 	Tokens.output_tagged_ident_string s
diff --git a/tools/coqworkmgr.ml b/tools/coqworkmgr.ml
index 68aadcfc..bfea141b 100644
--- a/tools/coqworkmgr.ml
+++ b/tools/coqworkmgr.ml
@@ -169,7 +169,7 @@ let main () =
     "-j",Arg.Set_int max_tokens, "max number of concurrent jobs";
     "-d",Arg.Set debug, "do not detach (debug)"] in
   let usage =
-    "Prints on stdout an env variable assignement to be picked up by coq\n"^
+    "Prints on stdout an env variable assignment to be picked up by coq\n"^
     "instances in order to limit the maximum number of concurrent workers.\n"^
     "The default value is 2.\n"^
     "Usage:" in
diff --git a/tools/fake_ide.ml b/tools/fake_ide.ml
index d48c6d0a..01620112 100644
--- a/tools/fake_ide.ml
+++ b/tools/fake_ide.ml
@@ -8,7 +8,7 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-(** Fake_ide : Simulate a [coqide] talking to a [coqtop -ideslave] *)
+(** Fake_ide : Simulate a [coqide] talking to a [coqidetop] *)
 
 let error s =
   prerr_endline ("fake_id: error: "^s);
@@ -284,7 +284,7 @@ let read_command inc = Parser.parse grammar inc
 
 let usage () =
   error (Printf.sprintf
-    "A fake coqide process talking to a coqtop -ideslave.\n\
+    "A fake coqide process talking to a coqtop -toploop coqidetop.\n\
      Usage: %s (file|-) [<coqtop>]\n\
      Input syntax is the following:\n%s\n"
      (Filename.basename Sys.argv.(0))
@@ -296,20 +296,8 @@ let main =
   if Sys.os_type = "Unix" then Sys.set_signal Sys.sigpipe
     (Sys.Signal_handle
        (fun _ -> prerr_endline "Broken Pipe (coqtop died ?)"; exit 1));
-  let def_args = ["--xml_format=Ppcmds"; "-ideslave"] in
-  let coqtop_name = (* from ide/ideutils.ml *)
-    let prog_name = "fake_ide" in
-    let len_prog_name = String.length prog_name in
-    let fake_ide_path = Sys.executable_name in
-    let fake_ide_path_len = String.length fake_ide_path in
-    let pos = fake_ide_path_len - len_prog_name in
-    let rex = Str.regexp_string prog_name in
-    try
-      let i = Str.search_backward rex fake_ide_path pos in
-      String.sub fake_ide_path 0 i ^ "coqtop" ^
-      String.sub fake_ide_path (i + len_prog_name)
-        (fake_ide_path_len - i - len_prog_name) 
-    with Not_found -> assert false in
+  let def_args = ["--xml_format=Ppcmds"] in
+  let idetop_name = System.get_toplevel_path "coqidetop" in
   let coqtop_args, input_file = match Sys.argv with
     | [| _; f |] -> Array.of_list def_args, f
     | [| _; f; ct |] ->
@@ -318,7 +306,7 @@ let main =
     | _ -> usage () in
   let inc = if input_file = "-" then stdin else open_in input_file in
   let coq =
-    let _p, cin, cout = Coqide.spawn coqtop_name coqtop_args in
+    let _p, cin, cout = Coqide.spawn idetop_name coqtop_args in
     let ip = Xml_parser.make (Xml_parser.SChannel cin) in
     let op = Xml_printer.make (Xml_printer.TChannel cout) in
     Xml_parser.check_eof ip false;
diff --git a/tools/gallina-db.el b/tools/gallina-db.el
deleted file mode 100644
index 9664f69f..00000000
--- a/tools/gallina-db.el
+++ /dev/null
@@ -1,240 +0,0 @@
-;;; gallina-db.el --- coq keywords database utility functions
-;;
-;; Author: Pierre Courtieu <courtieu@lri.fr>
-;; License:     GPL (GNU GENERAL PUBLIC LICENSE)
-;;
-
-;;; We store all information on keywords (tactics or command) in big
-;; tables (ex: `coq-tactics-db') From there we get: menus including
-;; "smart" commands, completions for command coq-insert-...
-;; abbrev tables and font-lock keyword
-
-;;; real value defined below
-
-;;; Commentary:
-;; 
-
-;;; Code:
-
-;(require 'proof-config)			; for proof-face-specs, a macro
-;(require 'holes)
-
-(defconst coq-syntax-db nil
-  "Documentation-only variable, for coq keyword databases.
-Each element of a keyword database contains the definition of a \"form\", of the
-form:
-
-(MENUNAME ABBREV INSERT STATECH KWREG INSERT-FUN HIDE)
-
-MENUNAME is the name of form (or form variant) as it should appear in menus or
-completion lists.
-
-ABBREV is the abbreviation for completion via \\[expand-abbrev].
-
-INSERT is the complete text of the form, which may contain holes denoted by
-\"#\" or \"@{xxx}\".
-
-If non-nil the optional STATECH specifies that the command is not state
-preserving for coq.
-
-If non-nil the optional KWREG is the regexp to colorize correponding to the
-keyword.  ex: \"simple\\\\s-+destruct\" (\\\\s-+ meaning \"one or more spaces\").
-*WARNING*: A regexp longer than another one should be put FIRST. For example:
-
-  (\"Module Type\" ... ... t \"Module\\s-+Type\")
-  (\"Module\" ... ... t \"Module\")
-
-Is ok because the longer regexp is recognized first.
-
-If non-nil the optional INSERT-FUN is the function to be called when inserting
-the form (instead of inserting INSERT, except when using \\[expand-abbrev]). This
-allows writing functions asking for more information to assist the user.
-
-If non-nil the optional HIDE specifies that this form should not appear in the
-menu but only in interactive completions.
-
-Example of what could be in your emacs init file:
-
-(defvar coq-user-tactics-db
-  '(
-    (\"mytac\" \"mt\" \"mytac # #\" t \"mytac\")
-    (\"myassert by\" \"massb\" \"myassert ( # : # ) by #\" t \"assert\")
-    ))
-
-Explanation of the first line: the tactic menu entry mytac, abbreviated by mt,
-will insert \"mytac # #\" where #s are holes to fill, and \"mytac\" becomes a
-new keyword to colorize." )
-
-(defun coq-insert-from-db (db prompt)
-  "Ask for a keyword, with completion on keyword database DB and insert.
-Insert corresponding string with holes at point.  If an insertion function is
-present for the keyword, call it instead.  see `coq-syntax-db' for DB
-structure."
-  (let* ((tac (completing-read (concat prompt " (tab for completion) : ")
-                               db nil nil))
-         (infos (cddr (assoc tac db)))
-         (s (car infos)) ; completion to insert
-         (f (car-safe (cdr-safe (cdr-safe (cdr infos))))) ; insertion function
-         (pt (point)))
-    (if f (funcall f) ; call f if present
-      (insert (or s tac)) ; insert completion and indent otherwise
-      (holes-replace-string-by-holes-backward-jump pt)
-      (indent-according-to-mode))))
-
-
-
-(defun coq-build-regexp-list-from-db (db &optional filter)
-  "Take a keyword database DB and return the list of regexps for font-lock.
-If non-nil Optional argument FILTER is a function applying to each line of DB.
-For each line if FILTER returns nil, then the keyword is not added to the
-regexp.  See `coq-syntax-db' for DB structure."
-  (let ((l db) (res ()))
-    (while l
-      (let* ((hd (car l)) (tl (cdr l))	; hd is the first infos list
-             (e1 (car hd)) (tl1 (cdr hd)) ; e1 = menu entry
-             (e2 (car tl1)) (tl2 (cdr tl1)) ; e2 = abbreviation
-             (e3 (car tl2)) (tl3 (cdr tl2)) ; e3 = completion
-             (e4 (car-safe tl3)) (tl4 (cdr-safe tl3)) ; e4 = state changing
-             (e5 (car-safe tl4)) (tl5 (cdr-safe tl4)) ; e5 = colorization string
-             )
-        ;; TODO delete doublons
-        (when (and e5 (or (not filter) (funcall filter hd)))
-          (setq res (nconc res (list e5)))) ; careful: nconc destructive!
-        (setq l tl)))
-    res
-    ))
-
-;; Computes the max length of strings in a list
-(defun max-length-db (db)
-  "Return the length of the longest first element (menu label) of DB.
-See `coq-syntax-db' for DB structure."
-  (let ((l db) (res 0))
-    (while l
-      (let ((lgth (length (car (car l)))))
-	(setq res (max lgth res))
-	(setq l (cdr l))))
-    res))
-
-
-
-(defun coq-build-menu-from-db-internal (db lgth menuwidth)
-  "Take a keyword database DB and return one insertion submenu.
-Argument LGTH is the max size of the submenu.  Argument MENUWIDTH is the width
-of the largest line in the menu (without abbrev and shortcut specifications).
-Used by `coq-build-menu-from-db', which you should probably use instead.  See
-`coq-syntax-db' for DB structure."
-  (let ((l db) (res ()) (size lgth)
-	(keybind-abbrev (substitute-command-keys " \\[expand-abbrev]")))
-    (while (and l (> size 0))
-      (let* ((hd (car l))(tl (cdr l))	; hd is a list of length 3 or 4
-	     (e1 (car hd)) (tl1 (cdr hd)) ; e1 = menu entry
-	     (e2 (car tl1)) (tl2 (cdr tl1)) ; e2 = abbreviation
-	     (e3 (car tl2)) (tl3 (cdr tl2)) ; e3 = completion
-	     (e4 (car-safe tl3)) (tl4 (cdr-safe tl3)) ; e4 = state changing
-	     (e5 (car-safe tl4)) (tl5 (cdr-safe tl4)) ; e5 = colorization string
-	     (e6 (car-safe tl5))	; e6 = function for smart insertion
-	     (e7 (car-safe (cdr-safe tl5))) ; e7 = if non-nil : hide in menu
-	     (entry-with (max (- menuwidth (length e1)) 0))
-	     (spaces (make-string entry-with ? ))
-	     ;;(restofmenu (coq-build-menu-from-db-internal tl (- size 1) menuwidth))
-	     )
-	(when (not e7) ;; if not hidden
-	  (let ((menu-entry
-		 (vector
-		  ;; menu entry label
-		  (concat e1 (if (not e2) "" (concat spaces "(" e2 keybind-abbrev ")")))
-		   ;;insertion function if present otherwise insert completion
-		   (if e6 e6 `(holes-insert-and-expand ,e3))
-		   t)))
-	    (setq res (nconc res (list menu-entry)))));; append *in place*
-	(setq l tl)
-	(setq size (- size 1))))
-    res))
-
-
-(defun coq-build-title-menu (db size)
-  "Build a title for the first submenu of DB, of size SIZE.
-Return the string made of the first and the SIZE nth first element of DB,
-separated by \"...\".  Used by `coq-build-menu-from-db'.  See `coq-syntax-db'
-for DB structure."
-    (concat (car-safe (car-safe db))
-	  " ... "
-	  (car-safe (car-safe (nthcdr (- size 1) db)))))
-
-(defun coq-sort-menu-entries (menu)
-  (sort menu 
-	(lambda (x y) (string< 
-			(downcase (elt x 0)) 
-			(downcase (elt y 0))))))
-
-(defun coq-build-menu-from-db (db &optional size)
-  "Take a keyword database DB and return a list of insertion menus for them.
-Submenus contain SIZE entries (default 30).  See `coq-syntax-db' for DB
-structure."
-  ;; sort is destructive for the list, so copy list before sorting
-  (let* ((l (coq-sort-menu-entries (copy-list db))) (res ())
-	 (wdth (+ 2 (max-length-db db)))
-	 (sz (or size 30)) (lgth (length l)))
-    (while l
-      (if (<= lgth sz)
-	  (setq res ;; careful: nconc destructive!
-		(nconc res (list (cons 
-				  (coq-build-title-menu l lgth)
-				  (coq-build-menu-from-db-internal l lgth wdth)))))
-	(setq res ; careful: nconc destructive!
-	      (nconc res (list (cons 
-				(coq-build-title-menu l sz)
-				(coq-build-menu-from-db-internal l sz wdth))))))
-      (setq l (nthcdr sz l))
-      (setq lgth (length l)))
-    res))
-
-(defun coq-build-abbrev-table-from-db (db)
-  "Take a keyword database DB and return an abbrev table.
-See `coq-syntax-db' for DB structure."
-  (let ((l db) (res ()))
-    (while l
-      (let* ((hd (car l))(tl (cdr l))	; hd is a list of length 3 or 4
-	     (e1 (car hd)) (tl1 (cdr hd)) ; e1 = menu entry
-	     (e2 (car tl1)) (tl2 (cdr tl1)) ; e2 = abbreviation
-	     (e3 (car tl2)) (tl3 (cdr tl2)) ; e3 = completion
-	     )
-	;; careful: nconc destructive!
-	(when e2 
-	  (setq res (nconc res (list `(,e2 ,e3 holes-abbrev-complete)))))
-	(setq l tl)))
-    res))
-
-
-(defun filter-state-preserving (l)
-  ; checkdoc-params: (l)
-  "Not documented."
-  (not (nth 3 l))) ; fourth argument is nil --> state preserving command
-
-(defun filter-state-changing (l)
-  ; checkdoc-params: (l)
-  "Not documented."
-  (nth 3 l)) ; fourth argument is nil --> state preserving command
-
-(defconst coq-solve-tactics-face 'coq-solve-tactics-face
-  "Expression that evaluates to a face.
-Required so that 'proof-solve-tactics-face is a proper facename")
-
-
-;;A new face for tactics which fail when they don't kill the current goal
-(defface coq-solve-tactics-face
-  '((t (:background "red")))
-  "Face for names of closing tactics in proof scripts."
-  :group 'proof-faces)
-
-
-
-
-
-(provide 'gallina-db)
-
-;;; gallina-db.el ends here
-
-;** Local Variables: ***
-;** fill-column: 80 ***
-;** End: ***
diff --git a/tools/gallina-syntax.el b/tools/gallina-syntax.el
deleted file mode 100644
index 662762b0..00000000
--- a/tools/gallina-syntax.el
+++ /dev/null
@@ -1,980 +0,0 @@
-;; gallina-syntax.el Font lock expressions for Coq
-;; Copyright (C) 1997-2007 LFCS Edinburgh. 
-;; Authors: Thomas Kleymann, Healfdene Goguen, Pierre Courtieu
-;; License:     GPL (GNU GENERAL PUBLIC LICENSE)
-;; Maintainer: Pierre Courtieu <courtieu@lri.fr>
-
-;; gallina-syntax.el,v 9.9 2008/07/21 15:14:58 pier Exp
-
-;(require 'proof-syntax)
-;(require 'proof-utils)                  ; proof-locate-executable
-(require 'gallina-db)
-
-
-
- ;;; keyword databases
-
-
-(defcustom coq-user-tactics-db nil
-  "User defined tactic information.  See `coq-syntax-db' for
- syntax. It is not necessary to add your own tactics here (it is not
- needed by the synchronizing/backtracking system). You may however do
- so for the following reasons:
-
-   1 your tactics will be colorized by font-lock
-
-   2 your tactics will be added to the menu and to completion when
-   calling \\[coq-insert-tactic]
-
-   3 you may define an abbreviation for your tactic."
-
-  :type '(repeat sexp)
-  :group 'coq)
-
-
-(defcustom coq-user-commands-db nil
-  "User defined command information.  See `coq-syntax-db' for
- syntax. It is not necessary to add your own commands here (it is not
- needed by the synchronizing/backtracking system). You may however do
- so for the following reasons:
-
-   1 your commands will be colorized by font-lock
-
-   2 your commands will be added to the menu and to completion when
-   calling \\[coq-insert-command]
-
-   3 you may define an abbreviation for your command."
-
-  :type '(repeat sexp)
-  :group 'coq)
-
-(defcustom coq-user-tacticals-db nil
-  "User defined tactical information.  See `coq-syntax-db' for
- syntax. It is not necessary to add your own commands here (it is not
- needed by the synchronizing/backtracking system). You may however do
- so for the following reasons:
-
-   1 your commands will be colorized by font-lock
-
-   2 your commands will be added to the menu and to completion when
-   calling \\[coq-insert-command]
-
-   3 you may define an abbreviation for your command."
-
-  :type '(repeat sexp)
-  :group 'coq)
-
-(defcustom coq-user-solve-tactics-db nil
-  "User defined closing tactics. See `coq-syntax-db' for
- syntax. It is not necessary to add your own commands here (it is not
- needed by the synchronizing/backtracking system). You may however do
- so for the following reasons:
-
-   1 your commands will be colorized by font-lock
-
-   2 your commands will be added to the menu and to completion when
-   calling \\[coq-insert-command]
-
-   3 you may define an abbreviation for your command."
-
-  :type '(repeat sexp)
-  :group 'coq)
-
-
-
-(defcustom coq-user-reserved-db nil
-  "User defined reserved keywords information.  See `coq-syntax-db' for
- syntax. It is not necessary to add your own commands here (it is not
- needed by the synchronizing/backtracking system). You may however do
- so for the following reasons:
-
-   1 your commands will be colorized by font-lock
-
-   2 your commands will be added to the menu and to completion when
-   calling \\[coq-insert-command]
-
-   3 you may define an abbreviation for your command."
-
-  :type '(repeat sexp)
-  :group 'coq)
-
-
-
-(defvar coq-tactics-db
-  (append 
-   coq-user-tactics-db
-   '(
-     ("absurd " "abs" "absurd " t "absurd")
-     ("apply" "ap" "apply " t "apply")
-     ("assert by" "assb" "assert ( # : # ) by #" t "assert")
-     ("assert" "ass" "assert ( # : # )" t)
-     ;;     ("assumption" "as" "assumption" t "assumption")
-     ("auto with arith" "awa" "auto with arith" t)
-     ("auto with" "aw" "auto with @{db}" t)
-     ("auto" "a" "auto" t "auto")
-     ("autorewrite with in using" "arwiu" "autorewrite with @{db,db...} in @{hyp} using @{tac}" t)
-     ("autorewrite with in" "arwi" "autorewrite with @{db,db...} in @{hyp}" t)
-     ("autorewrite with using" "arwu" "autorewrite with @{db,db...} using @{tac}" t)
-     ("autorewrite with" "ar" "autorewrite with @{db,db...}" t "autorewrite")
-     ("case" "c" "case " t "case")
-     ("cbv" "cbv" "cbv beta [#] delta iota zeta" t "cbv")
-     ("change in" "chi" "change # in #" t)
-     ("change with in" "chwi" "change # with # in #" t)
-     ("change with" "chw" "change # with" t)
-     ("change" "ch" "change " t "change")
-     ("clear" "cl" "clear" t "clear")
-     ("clearbody" "cl" "clearbody" t "clearbody")
-     ("cofix" "cof" "cofix" t "cofix")
-     ("coinduction" "coind" "coinduction" t "coinduction")
-     ("compare" "cmpa" "compare # #" t "compare")
-     ("compute" "cmpu" "compute" t "compute")
-     ;;     ("congruence" "cong" "congruence" t "congruence")
-     ("constructor" "cons" "constructor" t "constructor")
-     ;;     ("contradiction" "contr" "contradiction" t "contradiction")
-     ("cut" "cut" "cut" t "cut")
-     ("cutrewrite" "cutr" "cutrewrite -> # = #" t "cutrewrite")
-     ;;     ("decide equality" "deg" "decide equality" t "decide\\s-+equality")
-     ("decompose record" "decr" "decompose record #" t "decompose\\s-+record")
-     ("decompose sum" "decs" "decompose sum #" t "decompose\\s-+sum")
-     ("decompose" "dec" "decompose [#] #" t "decompose")
-     ("dependent inversion" "depinv" "dependent inversion" t "dependent\\s-+inversion")
-     ("dependent inversion with" "depinvw" "dependent inversion # with #" t)
-     ("dependent inversion_clear" "depinvc" "dependent inversion_clear" t "dependent\\s-+inversion_clear")
-     ("dependent inversion_clear with" "depinvw" "dependent inversion_clear # with #" t)
-     ("dependent rewrite ->" "depr" "dependent rewrite -> @{id}" t "dependent\\s-+rewrite")
-     ("dependent rewrite <-" "depr<" "dependent rewrite <- @{id}" t)
-     ("destruct as" "desa" "destruct # as #" t)
-     ("destruct using" "desu" "destruct # using #" t)
-     ("destruct" "des" "destruct " t  "destruct")
-     ;;     ("discriminate" "dis" "discriminate" t "discriminate")
-     ("discrR" "discrR" "discrR" t "discrR")
-     ("double induction" "dind" "double induction # #" t "double\\s-+induction")
-     ("eapply" "eap" "eapply #" t "eapply")
-     ("eauto with arith" "eawa" "eauto with arith" t)
-     ("eauto with" "eaw" "eauto with @{db}" t)
-     ("eauto" "ea" "eauto" t "eauto")
-     ("econstructor" "econs" "econstructor" t "econstructor")
-     ("eexists" "eex" "eexists" t "eexists")
-     ("eleft" "eleft" "eleft" t "eleft")
-     ("elim using" "elu" "elim # using #" t)
-     ("elim" "e" "elim #" t "elim")
-     ("elimtype" "elt" "elimtype" "elimtype")
-     ("eright" "erig" "eright" "eright")
-     ("esplit" "esp" "esplit" t "esplit")
-     ;;     ("exact" "exa" "exact" t "exact")
-     ("exists" "ex" "exists #" t "exists")
-     ;;     ("fail" "fa" "fail" nil)
-     ;;     ("field" "field" "field" t "field")
-     ("firstorder" "fsto" "firstorder" t "firstorder")
-     ("firstorder with" "fsto" "firstorder with #" t)
-     ("firstorder with using" "fsto" "firstorder # with #" t)
-     ("fold" "fold" "fold #" t "fold")
-     ;;     ("fourier" "four" "fourier" t "fourier")
-     ("functional induction" "fi" "functional induction @{f} @{args}" t "functional\\s-+induction")
-     ("generalize dependent" "gd" "generalize dependent #" t "generalize\\s-+dependent")
-     ("generalize" "g" "generalize #" t "generalize")
-     ("hnf" "hnf" "hnf" t "hnf")
-     ("idtac" "id" "idtac" nil "idtac") ; also in tacticals with abbrev id
-     ("idtac \"" "id\"" "idtac \"#\"")  ; also in tacticals
-     ("induction" "ind" "induction #" t "induction")
-     ("induction using" "indu" "induction # using #" t)
-     ("injection" "inj" "injection #" t "injection")
-     ("instantiate" "inst" "instantiate" t "instantiate")
-     ("intro" "i" "intro" t "intro")
-     ("intro after" "ia" "intro # after #" t)
-     ("intros" "is" "intros #" t "intros")
-     ("intros! (guess names)" nil "intros #" nil nil coq-insert-intros)
-     ("intros until" "isu" "intros until #" t)
-     ("intuition" "intu" "intuition #" t "intuition")
-     ("inversion" "inv" "inversion #" t "inversion")
-     ("inversion in" "invi" "inversion # in #" t)
-     ("inversion using" "invu" "inversion # using #" t)
-     ("inversion using in" "invui" "inversion # using # in #" t)
-     ("inversion_clear" "invcl" "inversion_clear" t "inversion_clear")
-     ("lapply" "lap" "lapply" t "lapply")
-     ("lazy" "lazy" "lazy beta [#] delta iota zeta" t "lazy")
-     ("left" "left" "left" t "left")
-     ("linear" "lin" "linear" t "linear")
-     ("load" "load" "load" t "load")
-     ("move after" "mov" "move # after #" t "move")
-     ("omega" "o" "omega" t "omega")
-     ("pattern" "pat" "pattern" t "pattern")
-     ("pattern(s)" "pats" "pattern # , #" t)
-     ("pattern at" "pata" "pattern # at #" t)
-     ("pose" "po" "pose ( # := # )" t "pose")
-     ("prolog" "prol" "prolog" t "prolog")
-     ("quote" "quote" "quote" t "quote")
-     ("quote []" "quote2" "quote # [#]" t)
-     ("red" "red" "red" t "red")
-     ("refine" "ref" "refine" t "refine")
-     ;;      ("reflexivity" "refl" "reflexivity #" t "reflexivity")
-     ("rename into" "ren" "rename # into #" t "rename")
-     ("replace with" "rep" "replace # with #" t "replace")
-     ("replace with in" "repi" "replace # with # in #" t)
-     ("rewrite <- in" "ri<" "rewrite <- # in #" t)
-     ("rewrite <-" "r<" "rewrite <- #" t)
-     ("rewrite in" "ri" "rewrite # in #" t)
-     ("rewrite" "r" "rewrite #" t "rewrite")
-     ("right" "rig" "right" t "right")
-     ;;      ("ring" "ring" "ring #" t "ring")
-     ("set in * |-" "seth" "set ( # := #) in * |-" t)
-     ("set in *" "set*" "set ( # := #) in *" t)
-     ("set in |- *" "setg" "set ( # := #) in |- *" t)
-     ("set in" "seti" "set ( # := #) in #" t)
-     ("set" "set" "set ( # := #)" t "set")
-     ("setoid_replace with" "strep2" "setoid_replace # with #" t "setoid_replace")
-     ("setoid replace with" "strep" "setoid replace # with #" t "setoid\\s-+replace")
-     ("setoid_rewrite" "strew" "setoid_rewrite #" t "setoid_rewrite")
-     ("setoid rewrite" "strew" "setoid rewrite #" t "setoid\\s-+rewrite")
-     ("simpl" "s" "simpl" t "simpl")
-     ("simpl" "sa" "simpl # at #" t)
-     ("simple destruct" "sdes" "simple destruct" t "simple\\s-+destruct")
-     ("simple inversion" "sinv" "simple inversion" t "simple\\s-+inversion")
-     ("simple induction" "sind" "simple induction" t "simple\\s-+induction")
-     ("simplify_eq" "simeq" "simplify_eq @{hyp}" t "simplify_eq")
-     ("specialize" "spec" "specialize" t "specialize")
-     ("split" "sp" "split" t "split")
-     ("split_Rabs" "spra" "splitRabs" t "split_Rabs")
-     ("split_Rmult" "sprm" "splitRmult" t "split_Rmult")
-     ("stepl" "stl" "stepl #" t "stepl")
-     ("stepl by" "stlb" "stepl # by #" t)
-     ("stepr" "str" "stepr #" t "stepr")
-     ("stepr by" "strb" "stepr # by #" t)
-     ("subst" "su" "subst #" t "subst")
-     ("symmetry" "sy" "symmetry" t "symmetry")
-     ("symmetry in" "syi" "symmetry in #" t)
-     ;;    ("tauto" "ta" "tauto" t "tauto")
-     ("transitivity" "trans" "transitivity #" t "transitivity")
-     ("trivial" "t" "trivial" t "trivial")
-     ("trivial with" "tw" "trivial with @{db}" t)
-     ("unfold" "u" "unfold #" t "unfold")
-     ("unfold(s)" "us" "unfold # , #" t)
-     ("unfold in" "unfi" "unfold # in #" t)
-     ("unfold at" "unfa" "unfold # at #" t)
-     ))
-  "Coq tactics information list. See `coq-syntax-db' for syntax. "
-  )
-
-(defvar coq-solve-tactics-db
-  (append
-   coq-user-solve-tactics-db
-   '(
-     ("assumption" "as" "assumption" t "assumption")
-     ("by" "by" "by #" t "by")
-     ("congruence" "cong" "congruence" t "congruence")
-     ("contradiction" "contr" "contradiction" t "contradiction")
-     ("decide equality" "deg" "decide equality" t "decide\\s-+equality")
-     ("discriminate" "dis" "discriminate" t "discriminate")
-     ("exact" "exa" "exact" t "exact")
-     ("fourier" "four" "fourier" t "fourier")
-     ("fail" "fa" "fail" nil)
-     ("field" "field" "field" t "field")
-     ("omega" "o" "omega" t "omega")
-     ("reflexivity" "refl" "reflexivity #" t "reflexivity")
-     ("ring" "ring" "ring #" t "ring")
-     ("solve" nil "solve [ # | # ]" nil "solve")
-     ("tauto" "ta" "tauto" t "tauto")
-     ))
-  "Coq tactic(al)s that solve a subgoal." 
-  )
-
-
-(defvar coq-tacticals-db
-  (append 
-   coq-user-tacticals-db
-   '(
-     ("info" nil "info #" nil "info")
-     ("first" nil "first [ # | # ]" nil "first")
-     ("abstract" nil "abstract @{tac} using @{name}." nil "abstract")
-     ("do" nil "do @{num} @{tac}" nil "do")
-     ("idtac" nil "idtac")              ; also in tactics
-                                        ;    ("idtac \"" nil "idtac \"#\"") ; also in tactics
-     ("fail" "fa" "fail" nil "fail")
-                                        ;    ("fail \"" "fa\"" "fail" nil) ;
-                                        ;    ("orelse" nil "orelse #" t "orelse")
-     ("repeat" nil "repeat #" nil "repeat")
-     ("try" nil "try #" nil "try")
-     ("progress" nil "progress #" nil "progress")
-     ("|" nil "[ # | # ]" nil)
-     ("||" nil "# || #" nil)
-     ))
-  "Coq tacticals information list.  See `coq-syntax-db' for syntax.")
-
-
-
-
-(defvar coq-decl-db
-  '(
-    ("Axiom" "ax" "Axiom # : #" t "Axiom")
-    ("Hint Constructors" "hc" "Hint Constructors # : #." t "Hint\\s-+Constructors")
-    ("Hint Extern" "he" "Hint Extern @{cost} @{pat} => @{tac} : @{db}." t "Hint\\s-+Extern")
-    ("Hint Immediate" "hi" "Hint Immediate # : @{db}." t "Hint\\s-+Immediate")
-    ("Hint Resolve" "hr" "Hint Resolve # : @{db}." t "Hint\\s-+Resolve")
-    ("Hint Rewrite ->" "hrw" "Hint Rewrite -> @{t1,t2...} using @{tac} : @{db}." t "Hint\\s-+Rewrite")
-    ("Hint Rewrite <-" "hrw" "Hint Rewrite <- @{t1,t2...} using @{tac} : @{db}." t )
-    ("Hint Unfold" "hu" "Hint Unfold # : #." t "Hint\\s-+Unfold")
-    ("Hypothesis" "hyp" "Hypothesis #: #" t "Hypothesis")
-    ("Hypotheses" "hyp" "Hypotheses #: #" t "Hypotheses")
-    ("Parameter" "par" "Parameter #: #" t "Parameter")
-    ("Parameters" "par" "Parameter #: #" t "Parameters")
-    ("Conjecture" "conj" "Conjecture #: #." t "Conjecture")
-    ("Variable" "v" "Variable #: #." t "Variable")
-    ("Variables" "vs" "Variables # , #: #." t "Variables")	
-    ("Coercion" "coerc" "Coercion @{id} : @{typ1} >-> @{typ2}." t "Coercion")
-    )
-  "Coq declaration keywords information list. See `coq-syntax-db' for syntax."
-  )
-
-(defvar coq-defn-db
-  '(
-    ("CoFixpoint" "cfix" "CoFixpoint # (#:#) : # :=\n#." t "CoFixpoint")
-    ("CoInductive" "coindv" "CoInductive # : # :=\n|# : #." t "CoInductive") 
-    ("Declare Module : :=" "dm" "Declare Module # : # := #." t "Declare\\s-+Module")
-    ("Declare Module <: :=" "dm2" "Declare Module # <: # := #." t);; careful
-    ("Declare Module Import : :=" "dmi" "Declare Module # : # := #." t)
-    ("Declare Module Import <: :=" "dmi2" "Declare Module # <: # := #." t);; careful
-    ("Declare Module Export : :=" "dme" "Declare Module # : # := #." t)
-    ("Declare Module Export <: :=" "dme2" "Declare Module # <: # := #." t);; careful
-    ("Definition" "def" "Definition #:# := #." t "Definition");; careful
-    ("Definition (2 args)" "def2" "Definition # (# : #) (# : #):# := #." t)
-    ("Definition (3 args)" "def3" "Definition # (# : #) (# : #) (# : #):# := #." t)
-    ("Definition (4 args)" "def4" "Definition # (# : #) (# : #) (# : #) (# : #):# := #." t)
-    ("Program Definition" "pdef" "Program Definition #:# := #." t "Program\\s-+Definition");; careful ?
-    ("Program Definition (2 args)" "pdef2" "Program Definition # (# : #) (# : #):# := #." t)
-    ("Program Definition (3 args)" "pdef3" "Program Definition # (# : #) (# : #) (# : #):# := #." t)
-    ("Program Definition (4 args)" "pdef4" "Program Definition # (# : #) (# : #) (# : #) (# : #):# := #." t)
-    ("Derive Inversion" nil "Derive Inversion @{id} with # Sort #." t "Derive\\s-+Inversion")
-    ("Derive Dependent Inversion" nil "Derive Dependent Inversion @{id} with # Sort #." t "Derive\\s-+Dependent\\s-+Inversion")
-    ("Derive Inversion_clear" nil "Derive Inversion_clear @{id} with # Sort #." t)
-    ("Fixpoint" "fix" "Fixpoint # (#:#) {struct @{arg}} : # :=\n#." t "Fixpoint")
-    ("Program Fixpoint" "pfix" "Program Fixpoint # (#:#) {struct @{arg}} : # :=\n#." t "Program\\s-+Fixpoint")
-    ("Program Fixpoint measure" "pfixm" "Program Fixpoint # (#:#) {measure @{arg} @{f}} : # :=\n#." t)
-    ("Program Fixpoint wf" "pfixwf" "Program Fixpoint # (#:#) {wf @{arg} @{f}} : # :=\n#." t)
-    ("Function" "func" "Function # (#:#) {struct @{arg}} : # :=\n#." t "Function")
-    ("Function measure" "funcm" "Function # (#:#) {measure @{f} @{arg}} : # :=\n#." t)
-    ("Function wf" "func wf" "Function # (#:#) {wf @{R} @{arg}} : # :=\n#." t)
-    ("Functional Scheme with" "fsw" "Functional Scheme @{name} := Induction for @{fun} with @{mutfuns}." t )
-    ("Functional Scheme" "fs" "Functional Scheme @{name} := Induction for @{fun}." t "Functional\\s-+Scheme")
-    ("Inductive" "indv" "Inductive # : # := # : #." t "Inductive")
-    ("Inductive (2 args)" "indv2" "Inductive # : # :=\n| # : #\n| # : #." t )
-    ("Inductive (3 args)" "indv3" "Inductive # : # :=\n| # : #\n| # : #\n| # : #." t )
-    ("Inductive (4 args)" "indv4" "Inductive # : # :=\n| # : #\n| # : #\n| # : #\n| # : #." t )
-    ("Inductive (5 args)" "indv5" "Inductive # : # :=\n| # : #\n| # : #\n| # : #\n| # : #\n| # : #." t )
-    ("Variant" "indv" "Variant # : # := # : #." t "Variant")
-    ("Variant (2 args)" "indv2" "Variant # : # :=\n| # : #\n| # : #." t )
-    ("Variant (3 args)" "indv3" "Variant # : # :=\n| # : #\n| # : #\n| # : #." t )
-    ("Variant (4 args)" "indv4" "Variant # : # :=\n| # : #\n| # : #\n| # : #\n| # : #." t )
-    ("Variant (5 args)" "indv5" "Variant # : # :=\n| # : #\n| # : #\n| # : #\n| # : #\n| # : #." t )
-    ("Let" "Let" "Let # : # := #." t "Let")
-    ("Ltac" "ltac" "Ltac # := #" t "Ltac")
-    ("Module :=" "mo" "Module # : # := #." t ) ; careful
-    ("Module <: :=" "mo2" "Module # <: # := #." t ) ; careful
-    ("Module Import :=" "moi" "Module Import # : # := #." t ) ; careful
-    ("Module Import <: :=" "moi2" "Module Import # <: # := #." t ) ; careful
-    ("Module Export :=" "moe" "Module Export # : # := #." t ) ; careful
-    ("Module Export <: :=" "moe2" "Module Export# <: # := #." t ) ; careful
-    ("Record" "rec" "Record # : # := {\n# : #;\n# : # }" t "Record")
-    ("Scheme" "sc" "Scheme @{name} := #." t "Scheme")
-    ("Scheme Induction" "sci" "Scheme @{name} := Induction for # Sort #." t)
-    ("Scheme Minimality" "scm" "Scheme @{name} := Minimality for # Sort #." t)
-    ("Structure" "str" "Structure # : # := {\n# : #;\n# : # }" t "Structure")	
-    )
-  "Coq definition keywords information list. See `coq-syntax-db' for syntax. "
-  )
-
-;; modules and section are indented like goal starters
-(defvar coq-goal-starters-db
-  '(
-    ("Add Morphism" "addmor" "Add Morphism @{f} : @{id}" t "Add\\s-+Morphism")
-    ("Chapter" "chp" "Chapter # : #." t "Chapter")
-    ("Corollary" "cor" "Corollary # : #.\nProof.\n#\nQed." t "Corollary")
-    ("Declare Module :" "dmi" "Declare Module # : #.\n#\nEnd #." t)
-    ("Declare Module <:" "dmi2" "Declare Module # <: #.\n#\nEnd #." t)
-    ("Definition goal" "defg" "Definition #:#.\n#\nQed." t);; careful
-    ("Fact" "fct" "Fact # : #." t "Fact")
-    ("Goal" nil "Goal #." t "Goal")
-    ("Lemma" "l" "Lemma # : #.\nProof.\n#\nQed." t "Lemma")
-    ("Program Lemma" "pl" "Program Lemma # : #.\nProof.\n#\nQed." t "Program\\s-+Lemma")
-    ("Module! (interactive)" nil "Module # : #.\n#\nEnd #." nil nil coq-insert-section-or-module)
-    ("Module Type" "mti" "Module Type #.\n#\nEnd #." t "Module\\s-+Type") ; careful
-    ("Module :" "moi" "Module # : #.\n#\nEnd #." t "Module") ; careful
-    ("Module <:" "moi2" "Module # <: #.\n#\nEnd #." t ) ; careful
-    ("Remark" "rk" "Remark # : #.\n#\nQed." t "Remark")
-    ("Section" "sec" "Section #." t "Section")
-    ("Theorem" "th" "Theorem # : #.\n#\nQed." t "Theorem")
-    ("Program Theorem" "pth" "Program Theorem # : #.\nProof.\n#\nQed." t "Program\\s-+Theorem")
-    ("Obligation" "obl" "Obligation #.\n#\nQed." t "Obligation")
-    ("Next Obligation" "nobl" "Next Obligation.\n#\nQed." t "Next Obligation")
-    )
-  "Coq goal starters keywords information list. See `coq-syntax-db' for syntax. "
-  )
-
-;; command that are not declarations, definition or goal starters
-(defvar coq-other-commands-db
-   '(
-     ;; ("Abort" nil "Abort." t "Abort" nil nil);don't appear in menu
-     ("About" nil "About #." nil "About")
-     ("Add" nil "Add #." nil "Add" nil t)
-     ("Add Abstract Ring" nil "Add Abstract Ring #." t "Add\\s-+Abstract\\s-+Ring")
-     ("Add Abstract Semi Ring" nil "Add Abstract Semi Ring #." t "Add\\s-+Abstract\\s-+Semi\\s-+Ring")
-     ("Add Field" nil "Add Field #." t "Add\\s-+Field")
-     ("Add LoadPath" nil "Add LoadPath #." nil "Add\\s-+LoadPath")
-     ("Add ML Path" nil "Add ML Path #." nil "Add\\s-+ML\\s-+Path")
-     ("Add Morphism" nil "Add Morphism #." t "Add\\s-+Morphism")
-     ("Add Printing" nil "Add Printing #." t "Add\\s-+Printing")
-     ("Add Printing Constructor" nil "Add Printing Constructor #." t "Add\\s-+Printing\\s-+Constructor")
-     ("Add Printing If" nil "Add Printing If #." t "Add\\s-+Printing\\s-+If")
-     ("Add Printing Let" nil "Add Printing Let #." t "Add\\s-+Printing\\s-+Let")
-     ("Add Printing Record" nil "Add Printing Record #." t "Add\\s-+Printing\\s-+Record")
-     ("Add Rec LoadPath" nil "Add Rec LoadPath #." nil "Add\\s-+Rec\\s-+LoadPath")
-     ("Add Rec ML Path" nil "Add Rec ML Path #." nil "Add\\s-+Rec\\s-+ML\\s-+Path")
-     ("Add Ring" nil "Add Ring #." t "Add\\s-+Ring")
-     ("Add Semi Ring" nil "Add Semi Ring #." t "Add\\s-+Semi\\s-+Ring")
-     ("Add Setoid" nil "Add Setoid #." t "Add\\s-+Setoid")
-     ("Admit Obligations" "oblsadmit" "Admit Obligations." nil "Admit\\s-+Obligations")
-     ("Arguments Scope" "argsc" "Arguments Scope @{id} [ @{_} ]" t "Arguments\\s-+Scope")
-     ("Bind Scope" "bndsc" "Bind Scope @{scope} with @{type}" t "Bind\\s-+Scope")
-     ("Canonical Structure" nil "Canonical Structure #." t "Canonical\\s-+Structure")
-     ("Cd" nil "Cd #." nil "Cd")
-     ("Check" nil "Check" nil "Check")
-     ("Close Local Scope" "cllsc" "Close Local Scope #" t "Close\\s-+Local\\s-+Scope")
-     ("Close Scope" "clsc" "Close Scope #" t "Close\\s-+Scope")
-     ("Comments" nil "Comments #." nil "Comments")
-     ("Delimit Scope" "delsc" "Delimit Scope @{scope} with @{id}." t "Delimit\\s-+Scope" )
-     ("Eval" nil "Eval #." nil "Eval")
-     ("Export" nil "Export #." t "Export")
-     ("Extract Constant" "extrc" "Extract Constant @{id} => \"@{id}\"." nil "Extract\\s-+Constant")
-     ("Extract Inlined Constant" "extric" "Extract Inlined Constant @{id} => \"@{id}\"." nil "Extract\\s-+Inlined\\s-+Constant")
-     ("Extract Inductive" "extri" "Extract Inductive @{id} => \"@{id}\" [\"@{id}\" \"@{id...}\"]." nil "Extract")
-     ("Extraction" "extr" "Extraction @{id}." nil "Extraction")
-     ("Extraction (in a file)" "extrf" "Extraction \"@{file}\" @{id}." nil)
-     ("Extraction Inline" nil "Extraction Inline #." t "Extraction\\s-+Inline")
-     ("Extraction NoInline" nil "Extraction NoInline #." t "Extraction\\s-+NoInline")
-     ("Extraction Language" "extrlang" "Extraction Language #." t "Extraction\\s-+Language")
-     ("Extraction Library" "extrl" "Extraction Library @{id}." nil "Extraction\\s-+Library")
-     ("Focus" nil "Focus #." nil "Focus")
-     ("Identity Coercion" nil "Identity Coercion #." t "Identity\\s-+Coercion")
-     ("Implicit Arguments Off" nil "Implicit Arguments Off." t "Implicit\\s-+Arguments\\s-+Off")
-     ("Implicit Arguments On" nil "Implicit Arguments On." t "Implicit\\s-+Arguments\\s-+On")
-     ("Implicit Arguments" nil "Implicit Arguments # [#]." t "Implicit\\s-+Arguments")
-     ("Import" nil "Import #." t "Import")
-     ("Infix" "inf" "Infix \"#\" := # (at level #) : @{scope}." t "Infix")
-     ("Inspect" nil "Inspect #." nil "Inspect")
-     ("Locate" nil "Locate" nil "Locate")
-     ("Locate File" nil "Locate File \"#\"." nil "Locate\\s-+File")
-     ("Locate Library" nil "Locate Library #." nil "Locate\\s-+Library")
-     ("Notation (assoc)" "notas" "Notation \"#\" := # (at level #, # associativity)." t)
-     ("Notation (at assoc)" "notassc" "Notation \"#\" := # (at level #, # associativity) : @{scope}." t)
-     ("Notation (at at scope)" "notasc" "Notation \"#\" := # (at level #, # at level #) : @{scope}." t)
-     ("Notation (at at)" "nota" "Notation \"#\" := # (at level #, # at level #)." t)
-     ("Notation (only parsing)" "notsp" "Notation # := # (only parsing)." t)
-     ("Notation Local (only parsing)" "notslp" "Notation Local # := # (only parsing)." t)
-     ("Notation Local" "notsl" "Notation Local # := #." t "Notation\\s-+Local")
-     ("Notation (simple)" "nots" "Notation # := #." t "Notation")
-     ("Opaque" nil "Opaque #." nil "Opaque")
-     ("Obligations Tactic" nil "Obligations Tactic := #." t "Obligations\\s-+Tactic")
-     ("Open Local Scope" "oplsc" "Open Local Scope #" t "Open\\s-+Local\\s-+Scope")
-     ("Open Scope" "opsc" "Open Scope #" t "Open\\s-+Scope")
-     ("Print Coercions" nil "Print Coercions." nil "Print\\s-+Coercions")
-     ("Print Hint" nil "Print Hint." nil "Print\\s-+Hint" coq-PrintHint)
-     ("Print" "p" "Print #." nil "Print")
-     ("Qed" nil "Qed." nil "Qed")
-     ("Pwd" nil "Pwd." nil "Pwd")
-     ("Recursive Extraction" "recextr" "Recursive Extraction @{id}." nil "Recursive\\s-+Extraction")
-     ("Recursive Extraction Library" "recextrl" "Recursive Extraction Library @{id}." nil "Recursive\\s-+Extraction\\s-+Library")
-     ("Recursive Extraction Module" "recextrm" "Recursive Extraction Module @{id}." nil "Recursive\\s-+Extraction\\s-+Module")
-     ("Remove LoadPath" nil "Remove LoadPath" nil "Remove\\s-+LoadPath")
-     ("Remove LoadPath" nil "Remove LoadPath" nil "Remove\\s-+LoadPath")
-     ("Remove Printing If" nil "Remove Printing If #." t "Remove\\s-+Printing\\s-+If")
-     ("Remove Printing Let" nil "Remove Printing Let #." t "Remove\\s-+Printing\\s-+Let")
-     ("Require Export" nil "Require Export #." t "Require\\s-+Export")
-     ("Require Import" nil "Require Import #." t "Require\\s-+Import")
-     ("Require" nil "Require #." t "Require")
-     ("Reserved Notation" nil "Reserved Notation" nil "Reserved\\s-+Notation")
-     ("Reset Extraction Inline" nil "Reset Extraction Inline." t "Reset\\s-+Extraction\\s-+Inline")
-     ("Search" nil "Search #" nil "Search")
-     ("SearchAbout" nil "SearchAbout #" nil "SearchAbout")
-     ("SearchPattern" nil "SearchPattern #" nil "SearchPattern")
-     ("SearchRewrite" nil "SearchRewrite #" nil "SearchRewrite")
-     ("Set Extraction AutoInline" nil "Set Extraction AutoInline" t "Set\\s-+Extraction\\s-+AutoInline")
-     ("Set Extraction Optimize" nil "Set Extraction Optimize" t "Set\\s-+Extraction\\s-+Optimize")
-     ("Set Implicit Arguments" nil "Set Implicit Arguments" t "Set\\s-+Implicit\\s-+Arguments")
-     ("Set Strict Implicit" nil "Set Strict Implicit" t "Set\\s-+Strict\\s-+Implicit")
-     ("Set Printing Synth" nil "Set Printing Synth" t "Set\\s-+Printing\\s-+Synth")
-     ("Set Printing Wildcard" nil "Set Printing Wildcard" t "Set\\s-+Printing\\s-+Wildcard")
-     ("Set Printing All" "sprall" "Set Printing All" t "Set\\s-+Printing\\s-+All")
-     ("Set Printing Records" nil "Set Printing Records" t "Set\\s-+Printing\\s-+Records")
-     ("Set Hyps Limit" nil "Set Hyps Limit #." nil "Set\\s-+Hyps\\s-+Limit")
-     ("Set Printing Coercions" nil "Set Printing Coercions." t "Set\\s-+Printing\\s-+Coercions")
-     ("Set Printing Notations" "sprn" "Set Printing Notations" t "Set\\s-+Printing\\s-+Notations")
-     ("Set Undo" nil "Set Undo #." nil "Set\\s-+Undo")
-     ("Show" nil "Show #." nil "Show")
-     ("Solve Obligations" "oblssolve" "Solve Obligations using #." nil "Solve\\s-+Obligations")
-     ("Test" nil "Test" nil "Test" nil t)
-     ("Test Printing Depth" nil "Test Printing Depth." nil "Test\\s-+Printing\\s-+Depth")
-     ("Test Printing If" nil "Test Printing If #." nil "Test\\s-+Printing\\s-+If")
-     ("Test Printing Let" nil "Test Printing Let #." nil "Test\\s-+Printing\\s-+Let")
-     ("Test Printing Synth" nil "Test Printing Synth." nil "Test\\s-+Printing\\s-+Synth")
-     ("Test Printing Width" nil "Test Printing Width." nil "Test\\s-+Printing\\s-+Width")
-     ("Test Printing Wildcard" nil "Test Printing Wildcard." nil "Test\\s-+Printing\\s-+Wildcard")
-     ("Transparent" nil "Transparent #." nil "Transparent")
-     ("Unfocus" nil "Unfocus." nil "Unfocus")
-     ("Unset Extraction AutoInline" nil "Unset Extraction AutoInline" t "Unset\\s-+Extraction\\s-+AutoInline")
-     ("Unset Extraction Optimize" nil "Unset Extraction Optimize" t "Unset\\s-+Extraction\\s-+Optimize")
-     ("Unset Implicit Arguments" nil "Unset Implicit Arguments" t "Unset\\s-+Implicit\\s-+Arguments")
-     ("Unset Strict Implicit" nil "Unset Strict Implicit" t "Unset\\s-+Strict\\s-+Implicit")
-     ("Unset Printing Synth" nil "Unset Printing Synth" t "Unset\\s-+Printing\\s-+Synth")
-     ("Unset Printing Wildcard" nil "Unset Printing Wildcard" t "Unset\\s-+Printing\\s-+Wildcard")
-     ("Unset Hyps Limit" nil "Unset Hyps Limit" nil "Unset\\s-+Hyps\\s-+Limit")
-     ("Unset Printing All" "unsprall" "Unset Printing All" nil "Unset\\s-+Printing\\s-+All")
-     ("Unset Printing Coercion" nil "Unset Printing Coercion #." t "Unset\\s-+Printing\\s-+Coercion")
-     ("Unset Printing Coercions" nil "Unset Printing Coercions." nil "Unset\\s-+Printing\\s-+Coercions")
-     ("Unset Printing Notations" "unsprn" "Unset Printing Notations" nil "Unset\\s-+Printing\\s-+Notations")
-     ("Unset Undo" nil "Unset Undo." nil "Unset\\s-+Undo")
- ;    ("print" "pr" "print #" "print")
-     )   
-   "Command that are not declarations, definition or goal starters."
-  )
-
-(defvar coq-commands-db
-  (append coq-decl-db coq-defn-db coq-goal-starters-db
-          coq-other-commands-db coq-user-commands-db)
-  "Coq all commands keywords information list. See `coq-syntax-db' for syntax. "      
-  )
-
-
-(defvar coq-terms-db
-  '(
-    ("fun (1 args)" "f" "fun #:# => #" nil "fun")
-    ("fun (2 args)" "f2" "fun (#:#) (#:#) => #")
-    ("fun (3 args)" "f3" "fun (#:#) (#:#) (#:#) => #")
-    ("fun (4 args)" "f4" "fun (#:#) (#:#) (#:#) (#:#) => #")
-    ("forall" "fo" "forall #:#,#" nil "forall")
-    ("forall (2 args)" "fo2" "forall (#:#) (#:#), #")
-    ("forall (3 args)" "fo3" "forall (#:#) (#:#) (#:#), #")
-    ("forall (4 args)" "fo4" "forall (#:#) (#:#) (#:#) (#:#), #")
-    ("if" "if" "if # then # else #" nil "if")
-    ("let in" "li" "let # := # in #" nil "let")
-    ("match! (from type)" nil "" nil "match" coq-insert-match)
-    ("match with" "m" "match # with\n| # => #\nend")
-    ("match with 2" "m2" "match # with\n| # => #\n| # => #\nend")
-    ("match with 3" "m3" "match # with\n| # => #\n| # => #\n| # => #\nend")
-    ("match with 4" "m4" "match # with\n| # => #\n| # => #\n| # => #\n| # => #\nend")
-    ("match with 5" "m5" "match # with\n| # => #\n| # => #\n| # => #\n| # => #\n| # => #\nend")
-    )
-  "Coq terms keywords information list. See `coq-syntax-db' for syntax. "
-  )
-
-
-
-
-
-
-
- ;;; Goals (and module/sections) starters detection
-
-
-;; ----- keywords for font-lock.
-
-;; FIXME da: this one function breaks the nice configuration of Proof General:
-;; would like to have proof-goal-regexp instead.
-;; Unfortunately Coq allows "Definition" and friends to perhaps have a goal, 
-;; so it appears more difficult than just a proof-goal-regexp setting.
-;; Future improvement may simply to be allow a function value for
-;; proof-goal-regexp.
-
-;; FIXME Pierre: the right way IMHO here would be to set a span
-;; property 'goalcommand when coq prompt says it (if the name of
-;; current proof has changed).
-
-;; excerpt of Jacek Chrzaszcz, implementer of the module system: sorry
-;; for the french:
-;;*) suivant les suggestions de Chritine, pas de mode preuve dans un type de
-;;    module (donc pas de Definition truc:machin.  Lemma, Theorem ... )
-;;
-;; *) la commande Module M [ ( : | <: ) MTYP ] [ := MEXPR ] est valable
-;;    uniquement hors d'un MT
-;;    - si :=MEXPR est absent, elle demarre un nouveau module interactif
-;;    - si :=MEXPR est present, elle definit un module
-;;    (la fonction vernac_define_module dans toplevel/vernacentries) 
-;;
-;; *) la nouvelle commande Declare Module M [ ( : | <: ) MTYP ] [ := MEXPR ]
-;;    est valable uniquement dans un MT
-;;    - si :=MEXPR absent, :MTYP absent, elle demarre un nouveau module
-;;      interactif
-;;    - si (:=MEXPR absent, :MTYP present) 
-;;      ou (:=MEXPR present, :MTYP absent)
-;;      elle declare un module.
-;;    (la fonction vernac_declare_module dans toplevel/vernacentries)
-
-(defun coq-count-match (regexp strg)
-  "Count the number of (maximum, non overlapping) matching substring 
- of STRG matching REGEXP. Empty match are counted once."
-  (let ((nbmatch 0) (str strg))
-    (while (and (proof-string-match regexp str) (not (string-equal str "")))
-      (incf nbmatch)
-      (if (= (match-end 0) 0) (setq str (substring str 1))
-        (setq str (substring str (match-end 0)))))
-    nbmatch))
-
-;; This function is used for amalgamating a proof into a single
-;; goal-save region (proof-goal-command-p used in
-;; proof-done-advancing-save in generic/proof-script.el) for coq <
-;; 8.0. It is the test when looking backward the start of the proof.
-;; It is NOT used for coq > v8.1
-;; (coq-find-and-forget in gallina.el uses state numbers, proof numbers and
-;; lemma names given in the prompt)
-
-;; compatibility with v8.0, will delete it some day
-(defun coq-goal-command-str-v80-p (str)
-  "See `coq-goal-command-p'."
-  (let* ((match (coq-count-match "\\<match\\>" str))
-	 (with (coq-count-match "\\<with\\>" str))
-	 (letwith (+ (coq-count-match "\\<let\\>" str) (- with match)))
-	 (affect (coq-count-match ":=" str)))
-
-    (and (proof-string-match coq-goal-command-regexp str)
- 	 (not				; 
- 	  (and 
- 	   (proof-string-match "\\`\\(Local\\|Definition\\|Lemma\\|Module\\)\\>" str)
- 	   (not (= letwith affect))))
- 	 (not (proof-string-match "\\`Declare\\s-+Module\\(\\w\\|\\s-\\|<\\)*:" str))
- 	 )
-    )
-  )
-
-;; Module and or section openings are detected syntactically. Module
-;; *openings* are difficult to detect because there can be Module
-;; ...with X := ... . So we need to count :='s to detect real openings.
-
-;; TODO: have opened section/chapter in the prompt too, and get rid of
-;; syntactical tests everywhere
-(defun coq-module-opening-p (str)
-  "Decide whether STR is a module or section opening or not. 
-Used by `coq-goal-command-p'"
-  (let* ((match (coq-count-match "\\<match\\>" str))
- 	 (with (coq-count-match "\\<with\\>" str))
- 	 (letwith (+ (coq-count-match "\\<let\\>" str) (- with match)))
- 	 (affect (coq-count-match ":=" str)))
-    (and (proof-string-match "\\`\\(Module\\)\\>" str)
- 	 (= letwith affect))
-    ))
-
-(defun coq-section-command-p (str)
-  (proof-string-match "\\`\\(Section\\|Chapter\\)\\>" str))
-
-
-(defun coq-goal-command-str-v81-p (str)
-  "Decide syntactically whether STR is a goal start or not. Use
-   `coq-goal-command-p-v81' on a span instead if possible."
-  (coq-goal-command-str-v80-p str)
-  )
-
-;; This is the function that tests if a SPAN is a goal start. All it
-;; has to do is look at the 'goalcmd attribute of the span.
-;; It also looks if this is not a module start.
-
-;; TODO: have also attributes 'modulecmd and 'sectioncmd. This needs
-;; something in the coq prompt telling the name of all opened modules
-;; (like for open goals), and use it to set goalcmd --> no more need
-;; to look at Modules and section (actually indentation will still
-;; need it)
-(defun coq-goal-command-p-v81 (span)
-  "see `coq-goal-command-p'"
-  (or (span-property span 'goalcmd)
-      ;; module and section starts are detected here
-      (let ((str (or (span-property span 'cmd) "")))
- 	(or (coq-section-command-p str)
- 	    (coq-module-opening-p str))
-        )))
-
-;; In coq > 8.1 This is used only for indentation.
-(defun coq-goal-command-str-p (str)
-  "Decide whether argument is a goal or not.  Use
-   `coq-goal-command-p' on a span instead if posible."
-  (cond 
-   (coq-version-is-V8-1 (coq-goal-command-str-v81-p str))
-   (coq-version-is-V8-0 (coq-goal-command-str-v80-p str))
-   (t (coq-goal-command-str-v80-p str));; this is temporary
-   ))
-
-;; This is used for backtracking
-(defun coq-goal-command-p (span)
-  "Decide whether argument is a goal or not."
-  (cond 
-   (coq-version-is-V8-1 (coq-goal-command-p-v81 span))
-   (coq-version-is-V8-0 (coq-goal-command-str-v80-p (span-property span 'cmd)))
-   (t (coq-goal-command-str-v80-p (span-property span 'cmd)));; this is temporary
-   ))
-
-(defvar coq-keywords-save-strict
-  '("Defined"
-    "Qed"
-    "End"
-    "Admitted"
-    "Abort"
-    ))
-
-(defvar coq-keywords-save
-  (append coq-keywords-save-strict '("Proof"))
-  )
-
-(defun coq-save-command-p (span str)
-  "Decide whether argument is a Save command or not"
-  (or (proof-string-match coq-save-command-regexp-strict str)
-      (and (proof-string-match "\\`Proof\\>" str)
-           (not (proof-string-match "Proof\\s-*\\(\\.\\|\\<with\\>\\)" str)))
-      )
-  )
-
-
-(defvar coq-keywords-kill-goal 
-  '("Abort"))
-
-;; Following regexps are all state changing
-(defvar coq-keywords-state-changing-misc-commands
-  (coq-build-regexp-list-from-db coq-commands-db 'filter-state-changing))
-
-(defvar coq-keywords-goal
-  (coq-build-regexp-list-from-db coq-goal-starters-db))
-
-(defvar coq-keywords-decl
-  (coq-build-regexp-list-from-db coq-decl-db))
-
-(defvar coq-keywords-defn
-  (coq-build-regexp-list-from-db coq-defn-db))
-
-
-(defvar coq-keywords-state-changing-commands
-  (append
-   coq-keywords-state-changing-misc-commands
-   coq-keywords-decl                    ; all state changing
-   coq-keywords-defn                    ; idem
-   coq-keywords-goal))                  ; idem
-
-
-;; 
-(defvar coq-keywords-state-preserving-commands
-  (coq-build-regexp-list-from-db coq-commands-db 'filter-state-preserving))
-
-;; concat this is faster that redoing coq-build-regexp-list-from-db on
-;; whole commands-db
-(defvar coq-keywords-commands
-  (append coq-keywords-state-changing-commands
- 	  coq-keywords-state-preserving-commands)
-  "All commands keyword.")
-
-(defvar coq-solve-tactics
-  (coq-build-regexp-list-from-db coq-solve-tactics-db)
-  "Keywords for closing tactic(al)s.")
-
-(defvar coq-tacticals
-  (coq-build-regexp-list-from-db coq-tacticals-db)
-  "Keywords for tacticals in a Coq script.")
-
-
- ;; From JF Monin:
-(defvar coq-reserved
-  (append 
-   coq-user-reserved-db
-   '(
-     "False" "True" "after" "as" "cofix" "fix" "forall" "fun" "match"
-     "return" "struct" "else" "end" "if" "in" "into" "let" "then"
-     "using" "with" "beta" "delta" "iota" "zeta" "after" "until"
-     "at" "Sort" "Time"))
-  "Reserved keywords of Coq.")
-
-
-(defvar coq-state-changing-tactics
-  (coq-build-regexp-list-from-db coq-tactics-db 'filter-state-changing))
-
-(defvar coq-state-preserving-tactics
-  (coq-build-regexp-list-from-db coq-tactics-db 'filter-state-preserving))
-
-
-(defvar coq-tactics
-  (append coq-state-changing-tactics coq-state-preserving-tactics))
-
-(defvar coq-retractable-instruct
-  (append coq-state-changing-tactics coq-keywords-state-changing-commands))
-
-(defvar coq-non-retractable-instruct
-  (append coq-state-preserving-tactics
-          coq-keywords-state-preserving-commands))
-
-(defvar coq-keywords
-  (append coq-keywords-goal coq-keywords-save coq-keywords-decl
- 	  coq-keywords-defn coq-keywords-commands)
-  "All keywords in a Coq script.")
-
-
-
-(defvar coq-symbols
-  '("|"
-    "||"
-    ":"
-    ";"
-    ","
-    "("
-    ")"
-    "["
-    "]"
-    "{"
-    "}"
-    ":="
-    "=>"
-    "->"
-    ".")
-  "Punctuation Symbols used by Coq.")
-
-;; ----- regular expressions
-(defvar coq-error-regexp "^\\(Error:\\|Discarding pattern\\|Syntax error:\\|System Error:\\|User Error:\\|User error:\\|Anomaly[:.]\\|Toplevel input[,]\\)"
-  "A regexp indicating that the Coq process has identified an error.")
-
-(defvar coq-id proof-id)
-(defvar coq-id-shy "\\(?:\\w\\(?:\\w\\|\\s_\\)*\\)")
-
-(defvar coq-ids (proof-ids coq-id " "))
-
-(defun coq-first-abstr-regexp (paren end)
-  (concat paren "\\s-*\\(" coq-ids "\\)\\s-*" end))
-
-(defcustom coq-variable-highlight-enable t
-  "Activates partial bound variable highlighting"
-  :type 'boolean
-  :group 'coq)
-
-
-(defvar coq-font-lock-terms
-  (if coq-variable-highlight-enable
-  (list
-   ;; lambda binders
-   (list (coq-first-abstr-regexp "\\<fun\\>" "\\(?:=>\\|:\\)") 1 'font-lock-variable-name-face)
-   ;; forall binder
-   (list (coq-first-abstr-regexp "\\<forall\\>" "\\(?:,\\|:\\)") 1 'font-lock-variable-name-face)
-                                        ;   (list "\\<forall\\>"
-                                        ;         (list 0 font-lock-type-face)
-                                        ;         (list (concat "[^ :]\\s-*\\(" coq-ids "\\)\\s-*") nil nil 
-                                        ;               (list 0 font-lock-variable-name-face)))
-   ;; parenthesized binders
-   (list (coq-first-abstr-regexp "(" ":[ a-zA-Z]") 1 'font-lock-variable-name-face)
-   ))
-  "*Font-lock table for Coq terms.")
-
-
-
-;; According to Coq, "Definition" is both a declaration and a goal.
-;; It is understood here as being a goal.  This is important for
-;; recognizing global identifiers, see coq-global-p.
-(defconst coq-save-command-regexp-strict
-  (proof-anchor-regexp 
-   (concat "\\(Time\\s-+\\|\\)\\(" (proof-ids-to-regexp coq-keywords-save-strict)
-           "\\)")))
-(defconst coq-save-command-regexp
-  (proof-anchor-regexp 
-   (concat "\\(Time\\s-+\\|\\)\\(" (proof-ids-to-regexp coq-keywords-save)
-           "\\)")))
-(defconst coq-save-with-hole-regexp
-  (concat "\\(Time\\s-+\\|\\)\\(" (proof-ids-to-regexp coq-keywords-save-strict)
- 	  "\\)\\s-+\\(" coq-id "\\)\\s-*\\."))
-
-(defconst coq-goal-command-regexp
-  (proof-anchor-regexp (proof-ids-to-regexp coq-keywords-goal)))
-
-(defconst coq-goal-with-hole-regexp
-  (concat "\\(" (proof-ids-to-regexp coq-keywords-goal)
- 	  "\\)\\s-+\\(" coq-id "\\)\\s-*:?"))
-
-(defconst coq-decl-with-hole-regexp
-  (concat "\\(" (proof-ids-to-regexp coq-keywords-decl)
- 	  "\\)\\s-+\\(" coq-ids "\\)\\s-*:"))
-
-;;  (defconst coq-decl-with-hole-regexp
-;;    (if coq-variable-highlight-enable coq-decl-with-hole-regexp-1 'nil))
-
-(defconst coq-defn-with-hole-regexp
-  (concat "\\(" (proof-ids-to-regexp coq-keywords-defn)
-          "\\)\\s-+\\(" coq-id "\\)"))
-
-;; must match:
-;; "with f x y :" (followed by = or not)
-;; "with f x y (z:" (not followed by =)
-;; BUT NOT:
-;; "with f ... (x:=" 
-;; "match ... with .. => "
-(defconst coq-with-with-hole-regexp
-  (concat "\\(with\\)\\s-+\\(" coq-id "\\)\\s-*\\([^=(.]*:\\|[^(]*(\\s-*" 
-          coq-id "\\s-*:[^=]\\)"))
-;; marche aussi a peu pres
-;;  (concat "\\(with\\)\\s-+\\(" coq-id "\\)\\s-*\\([^(.]*:\\|.*)[^(.]*:=\\)"))
-;;"\\<Prop\\>\\|\\<Set\\>\\|\\<Type\\>"
-(defvar coq-font-lock-keywords-1
-   (append
-    coq-font-lock-terms
-    (list
-    (cons (proof-ids-to-regexp coq-solve-tactics) 'coq-solve-tactics-face)
-    (cons (proof-ids-to-regexp coq-keywords) 'font-lock-keyword-face)
-    (cons (proof-ids-to-regexp coq-reserved) 'font-lock-type-face)
-    (cons (proof-ids-to-regexp coq-tactics ) 'proof-tactics-name-face)
-    (cons (proof-ids-to-regexp coq-tacticals) 'proof-tacticals-name-face)
-    (cons (proof-ids-to-regexp (list "Set" "Type" "Prop")) 'font-lock-type-face)
-    (cons "============================" 'font-lock-keyword-face)
-    (cons "Subtree proved!" 'font-lock-keyword-face)
-    (cons "subgoal [0-9]+ is:" 'font-lock-keyword-face)
-    (list "^\\([^ \n]+\\) \\(is defined\\)"
-          (list 2 'font-lock-keyword-face t)
-          (list 1 'font-lock-function-name-face t))
-
-    (list coq-goal-with-hole-regexp 2 'font-lock-function-name-face))
-    (if coq-variable-highlight-enable (list (list coq-decl-with-hole-regexp 2 'font-lock-variable-name-face)))
-    (list
-    (list coq-defn-with-hole-regexp 2 'font-lock-function-name-face)
-    (list coq-with-with-hole-regexp 2 'font-lock-function-name-face)
-    (list coq-save-with-hole-regexp 2 'font-lock-function-name-face)
-    ;; Remove spurious variable and function faces on commas.
-    '(proof-zap-commas))))
-
-(defvar coq-font-lock-keywords coq-font-lock-keywords-1)
-
-(defun coq-init-syntax-table ()
-  "Set appropriate values for syntax table in current buffer."
-
-  (modify-syntax-entry ?\$ ".")
-  (modify-syntax-entry ?\/ ".")
-  (modify-syntax-entry ?\\ ".")
-  (modify-syntax-entry ?+  ".")
-  (modify-syntax-entry ?-  ".")
-  (modify-syntax-entry ?=  ".")
-  (modify-syntax-entry ?%  ".")
-  (modify-syntax-entry ?<  ".")
-  (modify-syntax-entry ?>  ".")
-  (modify-syntax-entry ?\& ".")
-  (modify-syntax-entry ?_  "_")
-  (modify-syntax-entry ?\' "_")
-  (modify-syntax-entry ?\| ".")
-
-;; should maybe be "_" but it makes coq-find-and-forget (in gallina.el) bug
-  (modify-syntax-entry ?\. ".") 
-
-  (condition-case nil
-      ;; Try to use Emacs-21's nested comments.
-      (modify-syntax-entry ?\* ". 23n")
-    ;; Revert to non-nested comments if that failed.
-    (error (modify-syntax-entry ?\* ". 23")))
-  (modify-syntax-entry ?\( "()1")
-  (modify-syntax-entry ?\) ")(4"))
-
-
-(defconst coq-generic-expression
-  (mapcar (lambda (kw) 
- 	    (list (capitalize kw)
- 		  (concat "\\<" kw "\\>" "\\s-+\\(\\w+\\)\\W" )
- 		  1))
- 	  (append coq-keywords-decl coq-keywords-defn coq-keywords-goal)))
-
-(provide 'gallina-syntax)
- ;;; gallina-syntax.el ends here
-
-; Local Variables: ***
-; indent-tabs-mode: nil ***
-; End: ***
diff --git a/tools/gallina.el b/tools/gallina.el
deleted file mode 100644
index cbc13118..00000000
--- a/tools/gallina.el
+++ /dev/null
@@ -1,142 +0,0 @@
-;; gallina.el --- Coq mode editing commands for Emacs
-;;
-;; Jean-Christophe Filliatre, march 1995
-;; Shamelessly copied from caml.el, Xavier Leroy, july 1993.
-;;
-;; modified by Marco Maggesi <maggesi@math.unifi.it> for gallina-inferior
-
-; compatibility code for proofgeneral files
-(require 'coq-font-lock)
-; ProofGeneral files. remember to remove coq version tests in
-; gallina-syntax.el
-(require 'gallina-syntax)
-
-(defvar coq-mode-map nil
-  "Keymap used in Coq mode.")
-(if coq-mode-map
-    ()
-  (setq coq-mode-map (make-sparse-keymap))
-  (define-key coq-mode-map "\t"      'coq-indent-command)
-  (define-key coq-mode-map "\M-\t"   'coq-unindent-command)
-  (define-key coq-mode-map "\C-c\C-c"   'compile)
-)
-
-(defvar coq-mode-syntax-table nil
-  "Syntax table in use in Coq mode buffers.")
-(if coq-mode-syntax-table
-    ()
-  (setq coq-mode-syntax-table (make-syntax-table))
-  ; ( is first character of comment start
-  (modify-syntax-entry ?\( "()1" coq-mode-syntax-table)
-  ; * is second character of comment start,
-  ; and first character of comment end
-  (modify-syntax-entry ?*  ". 23" coq-mode-syntax-table)
-  ; ) is last character of comment end
-  (modify-syntax-entry ?\) ")(4" coq-mode-syntax-table)
-  ; quote is a string-like delimiter (for character literals)
-  (modify-syntax-entry ?' "\"" coq-mode-syntax-table)
-  ; quote is part of words
-  (modify-syntax-entry ?' "w" coq-mode-syntax-table)
-)
-
-(defvar coq-mode-indentation 2
-  "*Indentation for each extra tab in Coq mode.")
-
-(defun coq-mode-variables ()
-  (set-syntax-table coq-mode-syntax-table)
-  (make-local-variable 'paragraph-start)
-  (setq paragraph-start (concat "^$\\|" page-delimiter))
-  (make-local-variable 'paragraph-separate)
-  (setq paragraph-separate paragraph-start)
-  (make-local-variable 'paragraph-ignore-fill-prefix)
-  (setq paragraph-ignore-fill-prefix t)
-  (make-local-variable 'require-final-newline)
-  (setq require-final-newline t)
-  (make-local-variable 'comment-start)
-  (setq comment-start "(* ")
-  (make-local-variable 'comment-end)
-  (setq comment-end " *)")
-  (make-local-variable 'comment-column)
-  (setq comment-column 40)
-  (make-local-variable 'comment-start-skip)
-  (setq comment-start-skip "(\\*+ *")
-  (make-local-variable 'parse-sexp-ignore-comments)
-  (setq parse-sexp-ignore-comments nil)
-  (make-local-variable 'indent-line-function)
-  (setq indent-line-function 'coq-indent-command)
-  (make-local-variable 'font-lock-keywords)
-  (setq font-lock-defaults '(coq-font-lock-keywords-1)))
-
-;;; The major mode
-
-(defun coq-mode ()
-  "Major mode for editing Coq code.
-Tab at the beginning of a line indents this line like the line above.
-Extra tabs increase the indentation level.
-\\{coq-mode-map}
-The variable coq-mode-indentation indicates how many spaces are
-inserted for each indentation level."
-  (interactive)
-  (kill-all-local-variables)
-  (setq major-mode 'coq-mode)
-  (setq mode-name "coq")
-  (use-local-map coq-mode-map)
-  (coq-mode-variables)
-  (run-hooks 'coq-mode-hook))
-
-;;; Indentation stuff
-
-(defun coq-in-indentation ()
-  "Tests whether all characters between beginning of line and point
-are blanks."
-  (save-excursion
-    (skip-chars-backward " \t")
-    (bolp)))
-
-(defun coq-indent-command ()
-  "Indent the current line in Coq mode.
-When the point is at the beginning of an empty line, indent this line like
-the line above.
-When the point is at the beginning of an indented line
-\(i.e. all characters between beginning of line and point are blanks\),
-increase the indentation by one level.
-The indentation size is given by the variable coq-mode-indentation.
-In all other cases, insert a tabulation (using insert-tab)."
-  (interactive)
-  (let* ((begline
-          (save-excursion
-            (beginning-of-line)
-            (point)))
-         (current-offset
-          (- (point) begline))
-         (previous-indentation
-          (save-excursion
-            (if (eq (forward-line -1) 0) (current-indentation) 0))))
-    (cond ((and (bolp)
-                (looking-at "[ \t]*$")
-                (> previous-indentation 0))
-           (indent-to previous-indentation))
-          ((coq-in-indentation)
-           (indent-to (+ current-offset coq-mode-indentation)))
-          (t
-           (insert-tab)))))
-
-(defun coq-unindent-command ()
-  "Decrease indentation by one level in Coq mode.
-Works only if the point is at the beginning of an indented line
-\(i.e. all characters between beginning of line and point are blanks\).
-Does nothing otherwise."
-  (interactive)
-  (let* ((begline
-          (save-excursion
-            (beginning-of-line)
-            (point)))
-         (current-offset
-          (- (point) begline)))
-    (if (and (>= current-offset coq-mode-indentation)
-             (coq-in-indentation))
-        (backward-delete-char-untabify coq-mode-indentation))))
-
-;;; gallina.el ends here
-
-(provide 'gallina)
diff --git a/tools/gallina.ml b/tools/gallina.ml
deleted file mode 100644
index c7ff76be..00000000
--- a/tools/gallina.ml
+++ /dev/null
@@ -1,63 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
-(* <O___,, *       (see CREDITS file for the list of authors)           *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-open Gallina_lexer
-
-let vfiles = ref ([] : string list)
-
-let option_moins = ref false
-
-let option_stdout = ref false
-
-let traite_fichier f =
-  try
-    let chan_in = open_in (f^".v") in
-    let buf = Lexing.from_channel chan_in in
-    if not !option_stdout then chan_out := open_out (f ^ ".g");
-    try
-      while true do Gallina_lexer.action buf done
-    with Fin_fichier -> begin
-      flush !chan_out;
-      close_in chan_in;
-      if not !option_stdout then close_out !chan_out
-    end
-  with Sys_error _ ->
-    ()
-
-let traite_stdin () =
-  try
-    let buf = Lexing.from_channel stdin in
-    try
-      while true do Gallina_lexer.action buf done
-    with Fin_fichier ->
-      flush !chan_out
-  with Sys_error _ ->
-    ()
-
-let _ =
-  let lg_command = Array.length Sys.argv in
-  if lg_command < 2 then begin
-    output_string stderr "Usage: gallina [-] [-stdout] file1 file2 ...\n";
-    flush stderr;
-    exit 1
-  end;
-  let treat = function
-    | "-" -> option_moins := true
-    | "-stdout" -> option_stdout := true
-    | "-nocomments" -> comments := false
-    | f ->
-	if Filename.check_suffix f ".v" then
-       	  vfiles := (Filename.chop_suffix f ".v") :: !vfiles
-  in
-  Array.iter treat Sys.argv;
-  if !option_moins then
-    traite_stdin ()
-  else
-    List.iter traite_fichier !vfiles
diff --git a/tools/gallina_lexer.mll b/tools/gallina_lexer.mll
deleted file mode 100644
index 1a594aeb..00000000
--- a/tools/gallina_lexer.mll
+++ /dev/null
@@ -1,126 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
-(* <O___,, *       (see CREDITS file for the list of authors)           *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-{
-
- let chan_out = ref stdout
-
- let comment_depth = ref 0
- let cRcpt = ref 0
- let comments = ref true
- let print s = output_string !chan_out s
-
- exception Fin_fichier
-
-}
-
-let space = [' ' '\t' '\n' '\r']
-let enddot = '.' (' ' | '\t' | '\n' | '\r' | eof)
-
-rule action = parse
-  | "Theorem" space { print "Theorem "; body lexbuf;
-  	              cRcpt := 1; action lexbuf }
-  | "Lemma" space   { print "Lemma ";   body lexbuf;
-      	       	      cRcpt := 1; action lexbuf }
-  | "Fact" space    { print "Fact ";   body lexbuf;
-      	       	      cRcpt := 1; action lexbuf }
-  | "Remark" space  { print "Remark ";  body lexbuf;
-      	       	      cRcpt := 1; action lexbuf }
-  | "Goal" space    { print "Goal ";    body lexbuf;
-      	       	      cRcpt := 1; action lexbuf }
-  | "Correctness" space { print "Correctness "; body_pgm lexbuf;
-      	       	          cRcpt := 1; action lexbuf }
-  | "Definition" space  { print "Definition "; body_def lexbuf;
-			  cRcpt := 1; action lexbuf }
-  | "Hint" space        { skip_until_point lexbuf ; action lexbuf }
-  | "Hints" space        { skip_until_point lexbuf ; action lexbuf }
-  | "Transparent" space { skip_until_point lexbuf ; action lexbuf }
-  | "Immediate"	space   { skip_until_point lexbuf ; action lexbuf }
-  | "Syntax" space      { skip_until_point lexbuf ; action lexbuf }
-  | "(*"      { (if !comments then print "(*");
-		comment_depth := 1;
-      	        comment lexbuf;
-		cRcpt := 0; action lexbuf }
-  | [' ' '\t']* '\n'      { if !cRcpt < 2 then print "\n";
-      	       	       	    cRcpt := !cRcpt+1; action lexbuf}
-  | eof       { (raise Fin_fichier : unit)}
-  | _         { print (Lexing.lexeme lexbuf); cRcpt := 0; action lexbuf }
-
-and comment = parse
-  | "(*"  { (if !comments then print "(*");
-      	    comment_depth := succ !comment_depth; comment lexbuf }
-  | "*)"  { (if !comments then print "*)");
-      	    comment_depth := pred !comment_depth;
-            if !comment_depth > 0 then comment lexbuf }
-  | "*)" [' ''\t']*'\n' { (if !comments then print (Lexing.lexeme lexbuf));
-      			  comment_depth := pred !comment_depth;
-			  if !comment_depth > 0 then comment lexbuf }
-  | eof   { raise Fin_fichier }
-  | _     { (if !comments then print (Lexing.lexeme lexbuf));
-	    comment lexbuf }
-
-and skip_comment = parse
-  | "(*"  { comment_depth := succ !comment_depth; skip_comment lexbuf }
-  | "*)"  { comment_depth := pred !comment_depth;
-            if !comment_depth > 0 then skip_comment lexbuf }
-  | eof   { raise Fin_fichier }
-  | _     { skip_comment lexbuf }
-
-and body_def = parse
-  | [^'.']* ":=" { print (Lexing.lexeme lexbuf); () }
-  | _            { print (Lexing.lexeme lexbuf); body lexbuf }
-
-and body = parse
-  | enddot { print ".\n"; skip_proof lexbuf }
-  | ":="   { print ".\n"; skip_proof lexbuf }
-  | "(*"   { print "(*"; comment_depth := 1;
-      	     comment lexbuf; body lexbuf }
-  | eof    { raise Fin_fichier }
-  | _      { print (Lexing.lexeme lexbuf); body lexbuf }
-
-and body_pgm = parse
-  | enddot { print ".\n"; skip_proof lexbuf }
-  | "(*"   { print "(*"; comment_depth := 1;
-      	     comment lexbuf; body_pgm lexbuf }
-  | eof    { raise Fin_fichier }
-  | _      { print (Lexing.lexeme lexbuf); body_pgm lexbuf }
-
-and skip_until_point = parse
-  | '.' '\n' { () }
-  | enddot   { end_of_line lexbuf }
-  | "(*"     { comment_depth := 1;
-      	       skip_comment lexbuf; skip_until_point lexbuf }
-  | eof      { raise Fin_fichier }
-  | _        { skip_until_point lexbuf }
-
-and end_of_line = parse
-  | [' ' '\t' ]*	{ end_of_line lexbuf }
-  | '\n'		{ () }
-  | eof   	     	{ raise Fin_fichier }
-  | _	  		{ print (Lexing.lexeme lexbuf) }
-
-and skip_proof = parse
-  | "Save" space
-                { skip_until_point lexbuf }
-  | "Qed."  	{ end_of_line lexbuf }
-  | "Qed" space
-                { skip_until_point lexbuf }
-  | "Defined."  { end_of_line lexbuf }
-  | "Defined" space
-                { skip_until_point lexbuf }
-  | "Abort." 	{ end_of_line lexbuf }
-  | "Abort" space
-                { skip_until_point lexbuf }
-  | "Proof" space   { skip_until_point lexbuf }
-  | "Proof" [' ' '\t']* '.'  { skip_proof lexbuf }
-  | "(*"    { comment_depth := 1;
-      	      skip_comment lexbuf; skip_proof lexbuf }
-  | eof     { raise Fin_fichier }
-  | _       { skip_proof lexbuf }
diff --git a/tools/inferior-coq.el b/tools/inferior-coq.el
deleted file mode 100644
index 453bd139..00000000
--- a/tools/inferior-coq.el
+++ /dev/null
@@ -1,324 +0,0 @@
-;;; inferior-coq.el --- Run an inferior Coq process.
-;;;
-;;; Copyright (C) Marco Maggesi <maggesi@math.unifi.it>
-;;; Time-stamp: "2002-02-28 12:15:04 maggesi"
-
-
-;; Emacs Lisp Archive Entry
-;; Filename: inferior-coq.el
-;; Version: 1.0
-;; Keywords: process coq
-;; Author: Marco Maggesi <maggesi@math.unifi.it>
-;; Maintainer: Marco Maggesi <maggesi@math.unifi.it>
-;; Description: Run an inferior Coq process.
-;; URL: http://www.math.unifi.it/~maggesi/
-;; Compatibility: Emacs20, Emacs21, XEmacs21
-
-;; This is free software; you can redistribute it and/or modify it under
-;; the terms of the GNU General Public License as published by the Free
-;; Software Foundation; either version 2, or (at your option) any later
-;; version.
-;;
-;; This is distributed in the hope that it will be useful, but WITHOUT
-;; ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or
-;; FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public License
-;; for more details.
-;;
-;; You should have received a copy of the GNU General Public License
-;; along with GNU Emacs; see the file COPYING.  If not, write to the
-;; Free Software Foundation, Inc., 59 Temple Place - Suite 330, Boston,
-;; MA 02111-1307, USA.
-
-;;; Commentary:
-
-;; Coq is a proof assistant (http://coq.inria.fr/).  This code run an
-;; inferior Coq process and defines functions to send bits of code
-;; from other buffers to the inferior process.  This is a
-;; customisation of comint-mode (see comint.el).  For a more complex
-;; and full featured Coq interface under Emacs look at Proof General
-;; (http://zermelo.dcs.ed.ac.uk/~proofgen/).
-;;
-;; Written by Marco Maggesi <maggesi@math.unifi.it> with code heavly
-;; borrowed from emacs cmuscheme.el
-;;
-;; Please send me bug reports, bug fixes, and extensions, so that I can
-;; merge them into the master source.
-
-;;; Installation:
-
-;; You need to have gallina.el already installed (it comes with the
-;; standard Coq distribution) in order to use this code.  Put this
-;; file somewhere in you load-path and add the following lines in your
-;; "~/.emacs":
-;;
-;;   (setq auto-mode-alist (cons '("\\.v$" . coq-mode) auto-mode-alist))
-;;   (autoload 'coq-mode "gallina" "Major mode for editing Coq vernacular." t)
-;;   (autoload 'run-coq "inferior-coq" "Run an inferior Coq process." t)
-;;   (autoload 'run-coq-other-window "inferior-coq"
-;;     "Run an inferior Coq process in a new window." t)
-;;   (autoload 'run-coq-other-frame "inferior-coq"
-;;     "Run an inferior Coq process in a new frame." t)
-
-;;; Usage:
-
-;; Call `M-x "run-coq'.
-;;
-;; Functions and key bindings (Learn more keys with `C-c C-h' or `C-h m'):
-;;   C-return ('M-x coq-send-line)     send the current line.
-;;   C-c C-r  (`M-x coq-send-region')  send the current region.
-;;   C-c C-a  (`M-x coq-send-abort')   send the command "Abort".
-;;   C-c C-t  (`M-x coq-send-restart') send the command "Restart".
-;;   C-c C-s  (`M-x coq-send-show')    send the command "Show".
-;;   C-c C-u  (`M-x coq-send-undo')    send the command "Undo".
-;;   C-c C-v  (`M-x coq-check-region') run command "Check" on region.
-;;   C-c .    (`M-x coq-come-here')    Restart and send until current point.
-
-;;; Change Log:
-
-;; From -0.0 to 1.0 brought into existence.
-
-
-(require 'gallina)
-(require 'comint)
-
-(setq coq-program-name "coqtop")
-
-(defgroup inferior-coq nil
-  "Run a coq process in a buffer."
-  :group 'coq)
-
-(defcustom inferior-coq-mode-hook nil
-  "*Hook for customising inferior-coq mode."
-  :type 'hook
-  :group 'coq)
-
-(defvar inferior-coq-mode-map
-  (let ((m (make-sparse-keymap)))
-    (define-key m "\C-c\C-r" 'coq-send-region)
-    (define-key m "\C-c\C-a" 'coq-send-abort)
-    (define-key m "\C-c\C-t" 'coq-send-restart)
-    (define-key m "\C-c\C-s" 'coq-send-show)
-    (define-key m "\C-c\C-u" 'coq-send-undo)
-    (define-key m "\C-c\C-v" 'coq-check-region)
-    m))
-
-;; Install the process communication commands in the coq-mode keymap.
-(define-key coq-mode-map [(control return)] 'coq-send-line)
-(define-key coq-mode-map "\C-c\C-r" 'coq-send-region)
-(define-key coq-mode-map "\C-c\C-a" 'coq-send-abort)
-(define-key coq-mode-map "\C-c\C-t" 'coq-send-restart)
-(define-key coq-mode-map "\C-c\C-s" 'coq-send-show)
-(define-key coq-mode-map "\C-c\C-u" 'coq-send-undo)
-(define-key coq-mode-map "\C-c\C-v" 'coq-check-region)
-(define-key coq-mode-map "\C-c." 'coq-come-here)
-
-(defvar coq-buffer)
-
-(define-derived-mode inferior-coq-mode comint-mode "Inferior Coq"
-  "\
-Major mode for interacting with an inferior Coq process.
-
-The following commands are available:
-\\{inferior-coq-mode-map}
-
-A Coq process can be fired up with M-x run-coq.
-
-Customisation: Entry to this mode runs the hooks on comint-mode-hook
-and inferior-coq-mode-hook (in that order).
-
-You can send text to the inferior Coq process from other buffers
-containing Coq source.
-
-Functions and key bindings (Learn more keys with `C-c C-h'):
-  C-return ('M-x coq-send-line)     send the current line.
-  C-c C-r  (`M-x coq-send-region')  send the current region.
-  C-c C-a  (`M-x coq-send-abort')   send the command \"Abort\".
-  C-c C-t  (`M-x coq-send-restart') send the command \"Restart\".
-  C-c C-s  (`M-x coq-send-show')    send the command \"Show\".
-  C-c C-u  (`M-x coq-send-undo')    send the command \"Undo\".
-  C-c C-v  (`M-x coq-check-region') run command \"Check\" on region.
-  C-c .    (`M-x coq-come-here')    Restart and send until current point.
-"
-  ;; Customise in inferior-coq-mode-hook
-  (setq comint-prompt-regexp "^[^<]* < *")
-  (coq-mode-variables)
-  (setq mode-line-process '(":%s"))
-  (setq comint-input-filter (function coq-input-filter))
-  (setq comint-get-old-input (function coq-get-old-input)))
-
-(defcustom inferior-coq-filter-regexp "\\`\\s *\\S ?\\S ?\\s *\\'"
-  "*Input matching this regexp are not saved on the history list.
-Defaults to a regexp ignoring all inputs of 0, 1, or 2 letters."
-  :type 'regexp
-  :group 'inferior-coq)
-
-(defun coq-input-filter (str)
-  "Don't save anything matching `inferior-coq-filter-regexp'."
-  (not (string-match inferior-coq-filter-regexp str)))
-
-(defun coq-get-old-input ()
-  "Snarf the sexp ending at point."
-  (save-excursion
-    (let ((end (point)))
-      (backward-sexp)
-      (buffer-substring (point) end))))
-
-(defun coq-args-to-list (string)
-  (let ((where (string-match "[ \t]" string)))
-    (cond ((null where) (list string))
-	  ((not (= where 0))
-	   (cons (substring string 0 where)
-		 (coq-args-to-list (substring string (+ 1 where)
-						 (length string)))))
-	  (t (let ((pos (string-match "[^ \t]" string)))
-	       (if (null pos)
-		   nil
-		 (coq-args-to-list (substring string pos
-						 (length string)))))))))
-
-;;;###autoload
-(defun run-coq (cmd)
-  "Run an inferior Coq process, input and output via buffer *coq*.
-If there is a process already running in `*coq*', switch to that buffer.
-With argument, allows you to edit the command line (default is value
-of `coq-program-name').  Runs the hooks `inferior-coq-mode-hook'
-\(after the `comint-mode-hook' is run).
-\(Type \\[describe-mode] in the process buffer for a list of commands.)"
-
-  (interactive (list (if current-prefix-arg
-			 (read-string "Run Coq: " coq-program-name)
-			 coq-program-name)))
-  (if (not (comint-check-proc "*coq*"))
-      (let ((cmdlist (coq-args-to-list cmd)))
-	(set-buffer (apply 'make-comint "coq" (car cmdlist)
-			   nil (cdr cmdlist)))
-	(inferior-coq-mode)))
-  (setq coq-program-name cmd)
-  (setq coq-buffer "*coq*")
-  (switch-to-buffer "*coq*"))
-;;;###autoload (add-hook 'same-window-buffer-names "*coq*")
-
-;;;###autoload
-(defun run-coq-other-window (cmd)
-  "Run an inferior Coq process, input and output via buffer *coq*.
-If there is a process already running in `*coq*', switch to that buffer.
-With argument, allows you to edit the command line (default is value
-of `coq-program-name').  Runs the hooks `inferior-coq-mode-hook'
-\(after the `comint-mode-hook' is run).
-\(Type \\[describe-mode] in the process buffer for a list of commands.)"
-
-  (interactive (list (if current-prefix-arg
-			 (read-string "Run Coq: " coq-program-name)
-			 coq-program-name)))
-  (if (not (comint-check-proc "*coq*"))
-      (let ((cmdlist (coq-args-to-list cmd)))
-	(set-buffer (apply 'make-comint "coq" (car cmdlist)
-			   nil (cdr cmdlist)))
-	(inferior-coq-mode)))
-  (setq coq-program-name cmd)
-  (setq coq-buffer "*coq*")
-  (pop-to-buffer "*coq*"))
-;;;###autoload (add-hook 'same-window-buffer-names "*coq*")
-
-(defun run-coq-other-frame (cmd)
-  "Run an inferior Coq process, input and output via buffer *coq*.
-If there is a process already running in `*coq*', switch to that buffer.
-With argument, allows you to edit the command line (default is value
-of `coq-program-name').  Runs the hooks `inferior-coq-mode-hook'
-\(after the `comint-mode-hook' is run).
-\(Type \\[describe-mode] in the process buffer for a list of commands.)"
-
-  (interactive (list (if current-prefix-arg
-			 (read-string "Run Coq: " coq-program-name)
-			 coq-program-name)))
-  (if (not (comint-check-proc "*coq*"))
-      (let ((cmdlist (coq-args-to-list cmd)))
-	(set-buffer (apply 'make-comint "coq" (car cmdlist)
-			   nil (cdr cmdlist)))
-	(inferior-coq-mode)))
-  (setq coq-program-name cmd)
-  (setq coq-buffer "*coq*")
-  (switch-to-buffer-other-frame "*coq*"))
-
-(defun switch-to-coq (eob-p)
-  "Switch to the coq process buffer.
-With argument, position cursor at end of buffer."
-  (interactive "P")
-  (if (get-buffer coq-buffer)
-      (pop-to-buffer coq-buffer)
-      (error "No current process buffer.  See variable `coq-buffer'"))
-  (cond (eob-p
-	 (push-mark)
-	 (goto-char (point-max)))))
-
-(defun coq-send-region (start end)
-  "Send the current region to the inferior Coq process."
-  (interactive "r")
-  (comint-send-region (coq-proc) start end)
-  (comint-send-string (coq-proc) "\n"))
-
-(defun coq-send-line ()
-  "Send the current line to the Coq process."
-  (interactive)
-  (save-excursion
-    (end-of-line)
-    (let ((end (point)))
-      (beginning-of-line)
-      (coq-send-region (point) end)))
-  (forward-line 1))
-
-(defun coq-send-abort ()
-  "Send the command \"Abort.\" to the inferior Coq process."
-  (interactive)
-  (comint-send-string (coq-proc) "Abort.\n"))
-
-(defun coq-send-restart ()
-  "Send the command \"Restart.\" to the inferior Coq process."
-  (interactive)
-  (comint-send-string (coq-proc) "Restart.\n"))
-
-(defun coq-send-undo ()
-  "Reset coq to the initial state and send the region between the
-   beginning of file and the point."
-  (interactive)
-  (comint-send-string (coq-proc) "Undo.\n"))
-
-(defun coq-check-region (start end)
-  "Run the commmand \"Check\" on the current region."
-  (interactive "r")
-  (comint-proc-query (coq-proc)
-		     (concat "Check "
-			     (buffer-substring start end)
-			     ".\n")))
-
-(defun coq-send-show ()
-  "Send the command \"Show.\" to the inferior Coq process."
-  (interactive)
-  (comint-send-string (coq-proc) "Show.\n"))
-
-(defun coq-come-here ()
-  "Reset coq to the initial state and send the region between the
-   beginning of file and the point."
-  (interactive)
-  (comint-send-string (coq-proc) "Reset Initial.\n")
-  (coq-send-region 1 (point)))
-
-(defvar coq-buffer nil "*The current coq process buffer.")
-
-(defun coq-proc ()
-  "Return the current coq process.  See variable `coq-buffer'."
-  (let ((proc (get-buffer-process (if (eq major-mode 'inferior-coq-mode)
-				      (current-buffer)
-				      coq-buffer))))
-    (or proc
-	(error "No current process.  See variable `coq-buffer'"))))
-
-(defcustom inferior-coq-load-hook nil
-  "This hook is run when inferior-coq is loaded in.
-This is a good place to put keybindings."
-  :type 'hook
-  :group 'inferior-coq)
-	
-(run-hooks 'inferior-coq-load-hook)
-
-(provide 'inferior-coq)