Goodbye typerex, Hello merlin

4 files changed, 47 insertions, 27 deletions

diff --git a/.merlin b/.merlin
new file mode 100644
index 000000000..929f98e2c
--- /dev/null
+++ b/.merlin
@@ -0,0 +1,40 @@
+FLG -rectypes
+
+S lib
+B lib
+S intf
+B intf
+S kernel
+B kernel
+S kernel/byterun
+B kernel/byterun
+S library
+B library
+S pretyping
+B pretyping
+S interp
+B interp
+S proofs
+B proofs
+S tactics
+B tactics
+S parsing
+B parsing
+S toplevel
+B toplevel
+S plugins
+B plugins
+
+S ide
+B ide
+S ide/utils
+B ide/utils
+S tools
+B tools
+S tools/coqdoc
+B tools/coqdoc
+S dev
+B dev
+
+S checker
+B checker
diff --git a/.typerex b/.typerex
deleted file mode 100644
index 95921c8fa..000000000
--- a/.typerex
+++ /dev/null
@@ -1,17 +0,0 @@
-parsing
-ide
-ide/utils
-interp
-kernel
-kernel/byterun
-lib
-library
-plugins
-pretyping
-proofs
-states
-tactics
-theories
-tools
-tools/coqdoc
-toplevel
\ No newline at end of file
diff --git a/Makefile.build b/Makefile.build
index face3e34d..ba4ed52b5 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -103,8 +103,8 @@ HIDE := $(if $(VERBOSE),,@)
 LOCALINCLUDES=$(addprefix -I , $(SRCDIRS) )
 MLINCLUDES=$(LOCALINCLUDES) -I $(MYCAMLP4LIB)
 
-OCAMLC := $(TYPEREX) $(OCAMLC) $(CAMLFLAGS)
-OCAMLOPT := $(TYPEREX) $(OCAMLOPT) $(CAMLFLAGS)
+OCAMLC := $(OCAMLC) $(CAMLFLAGS)
+OCAMLOPT := $(OCAMLOPT) $(CAMLFLAGS)
 
 BYTEFLAGS=$(CAMLDEBUG) $(USERFLAGS)
 OPTFLAGS=$(CAMLDEBUGOPT) $(CAMLTIMEPROF) $(USERFLAGS)
diff --git a/configure.ml b/configure.ml
index 6e0b610fc..312d442bc 100644
--- a/configure.ml
+++ b/configure.ml
@@ -229,7 +229,6 @@ module Prefs = struct
   let debug = ref false
   let profile = ref false
   let annotate = ref false
-  let typerex = ref false
   let makecmd = ref "make"
   let nativecompiler = ref true
   let coqwebsite = ref "http://coq.inria.fr/"
@@ -307,9 +306,7 @@ let args_options = Arg.align [
   "-profile", Arg.Set Prefs.profile,
     " Add profiling information in the Coq executables";
   "-annotate", Arg.Set Prefs.annotate,
-    " Compiles Coq with -dtypes option";
-  "-typerex", Arg.Set Prefs.typerex,
-    " Compiles Coq using typerex wrapper";
+    " Dumps ml annotation files while compiling Coq";
   "-makecmd", Arg.Set_string Prefs.makecmd,
     "<command> Name of GNU Make command";
   "-no-native-compiler", Arg.Clear Prefs.nativecompiler,
@@ -369,9 +366,10 @@ let rebase_camlexec dir c =
 
 let coq_debug_flag = if !Prefs.debug then "-g" else ""
 let coq_profile_flag = if !Prefs.profile then "-p" else ""
-let coq_annotate_flag = if !Prefs.annotate then "-dtypes" else ""
-let coq_typerex_wrapper =
-  if !Prefs.typerex then "ocb-wrapper -save-types" else ""
+let coq_annotate_flag =
+  if !Prefs.annotate
+  then if program_in_path "ocamlmerlin" then "-bin-annot" else "-dtypes"
+  else ""
 
 let cflags = "-fno-defer-pop -Wall -Wno-unused"
 
@@ -1068,7 +1066,6 @@ let write_makefile f =
   pr "CAMLOPTLINK=%S\n\n" camlexec.opt;
   pr "# Caml flags\n";
   pr "CAMLFLAGS=-rectypes %s\n" coq_annotate_flag;
-  pr "TYPEREX=%s\n\n" coq_typerex_wrapper;
   pr "# User compilation flag\n";
   pr "USERFLAGS=\n\n";
   pr "# Flags for GCC\n";