remove -rectypes except for term.ml

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15871 85f007b7-540e-0410-9357-904b9bb8a0f7

8 files changed, 40 insertions, 72 deletions

diff --git a/Makefile.build b/Makefile.build
index cb5672cae5..0cc9466453 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -678,12 +678,12 @@ install-latex:
 source-doc: mli-doc $(OCAMLDOCDIR)/coq.pdf
 
 $(OCAMLDOCDIR)/coq.tex:: $(DOCMLIS:.mli=.cmi)
-	$(OCAMLDOC) -latex -rectypes -I $(MYCAMLP4LIB) $(MLINCLUDES)\
+	$(OCAMLDOC) -latex -I $(MYCAMLP4LIB) $(MLINCLUDES)\
 	$(DOCMLIS) -t "Coq mlis documentation" \
 	-intro $(OCAMLDOCDIR)/docintro -o $@
 
 mli-doc:: $(DOCMLIS:.mli=.cmi)
-	$(OCAMLDOC) -html -rectypes -I $(MYCAMLP4LIB) $(MLINCLUDES)\
+	$(OCAMLDOC) -html -I $(MYCAMLP4LIB) $(MLINCLUDES)\
 	$(DOCMLIS) -d $(OCAMLDOCDIR)/html -colorize-code \
 	-t "Coq mlis documentation" -intro $(OCAMLDOCDIR)/docintro \
 	-css-style style.css
@@ -696,9 +696,9 @@ ml-dot:: $(MLEXTRAFILES)
 	$(DOT) -Tpng $< -o $@
 
 %_types.dot: %.mli
-	$(OCAMLDOC) -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -dot-types -o $@ $< 
+	$(OCAMLDOC) $(MLINCLUDES) $(ODOCDOTOPTS) -dot-types -o $@ $<
 
-OCAMLDOC_MLLIBD = $(OCAMLDOC) -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -o $@ \
+OCAMLDOC_MLLIBD = $(OCAMLDOC) $(MLINCLUDES) $(ODOCDOTOPTS) -o $@ \
   $(foreach lib,$(|:.mllib.d=_MLLIB_DEPENDENCIES),$(addsuffix .ml,$($(lib))))
 
 %.dot: | %.mllib.d
@@ -717,7 +717,7 @@ tactics/tactics.dot: | tactics/tactics.mllib.d tactics/hightactics.mllib.d
 	$(OCAMLDOC_MLLIBD)
 
 %.dot: %.mli
-	$(OCAMLDOC) -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -o $@ $< 
+	$(OCAMLDOC) $(MLINCLUDES) $(ODOCDOTOPTS) -o $@ $<
 
 $(OCAMLDOCDIR)/%.pdf: $(OCAMLDOCDIR)/%.tex
 	(cd $(OCAMLDOCDIR) ; pdflatex $*.tex && pdflatex $*.tex)
@@ -748,15 +748,17 @@ grammar/grammar.cma: | grammar/grammar.mllib.d
 ## as dependency file, be sure to import the same modules in the different sections
 ## of the ml4
 
-toplevel/mltop.cmx: toplevel/mltop.optml | toplevel/mltop.ml.d toplevel/mltop.ml4.d
+MLTOP:=toplevel/mltop
+
+$(MLTOP).cmx: $(MLTOP).optml | $(MLTOP).ml.d $(MLTOP).ml4.d
 	$(SHOW)'OCAMLOPT  $<'
 	$(HIDE)$(OCAMLOPT) $(OPTFLAGS) -c -impl $< -o $@
 
-toplevel/mltop.ml: toplevel/mltop.ml4 config/Makefile # no camlp4deps here
+$(MLTOP).ml: $(MLTOP).ml4 config/Makefile # no camlp4deps here
 	$(SHOW)'CAMLP4O   $<'
 	$(HIDE)$(CAMLP4O) $(PR_O) $(CAMLP4USE) -DByte -DHasDynlink -impl $< -o $@
 
-toplevel/mltop.optml: toplevel/mltop.ml4 config/Makefile # no camlp4deps here
+$(MLTOP).optml: $(MLTOP).ml4 config/Makefile # no camlp4deps here
 	$(SHOW)'CAMLP4O   $<'
 	$(HIDE)$(CAMLP4O) $(PR_O) $(CAMLP4USE) $(NATDYNLINKDEF) -impl $< -o $@
 
@@ -768,6 +770,18 @@ ide/coqide_main_opt.ml: ide/coqide_main.ml4 config/Makefile # no camlp4deps here
 	$(SHOW)'CAMLP4O   $<'
 	$(HIDE)$(CAMLP4O) $(PR_O) $(CAMLP4USE) -D$(IDEOPTINT) -impl $< -o $@
 
+# Specific rule for term.ml which uses -rectypes
+# Since term.mli doesn't need -rectypes, this doesn't impact the other ml files
+
+TERM:=kernel/term
+
+$(TERM).cmo: $(TERM).ml | $(TERM).ml.d
+	$(SHOW)'OCAMLC -rectypes $<'
+	$(HIDE)$(OCAMLC) $(BYTEFLAGS) -rectypes -c $<
+
+$(TERM).cmx: $(TERM).ml | $(TERM).ml.d
+	$(SHOW)'OCAMLOPT -rectypes $<'
+	$(HIDE)$(OCAMLOPT) $(OPTFLAGS) -intf-suffix .cmi -rectypes -c $<
 
 # pretty printing of the revision number when compiling a checked out
 # source tree
diff --git a/_tags b/_tags
index ca0d9e7b81..767b6ebe29 100644
--- a/_tags
+++ b/_tags
@@ -22,6 +22,10 @@
 
 <grammar/grammar.{cma,cmxa}> : use_unix
 
+## tags for ml files
+
+"kernel/term.ml": rectypes
+
 ## tags for camlp4 files 
 
 "toplevel/mltop.ml4": is_mltop
diff --git a/configure b/configure
index 9a002198df..f4b5b7e2ff 100755
--- a/configure
+++ b/configure
@@ -1118,7 +1118,7 @@ CAMLLINK="$bytecamlc"
 CAMLOPTLINK="$nativecamlc"
 
 # Caml flags
-CAMLFLAGS=-rectypes $coq_annotate_flag
+CAMLFLAGS=$coq_annotate_flag
 TYPEREX=$coq_typerex_wrapper
 
 # Compilation debug flags
diff --git a/dev/doc/debugging.txt b/dev/doc/debugging.txt
index 2480b8edb3..83512c658b 100644
--- a/dev/doc/debugging.txt
+++ b/dev/doc/debugging.txt
@@ -21,15 +21,6 @@ Debugging from Coq toplevel using Caml trace mechanism
   notations, ...), use "Set Printing All". It will affect the #trace
   printers too.
 
-Note for Ocaml 3.10.x: Ocaml 3.10.x requires that modules compiled
-with -rectypes are loaded in an environment with -rectypes set but
-there is no way to tell the toplevel to support -rectypes. To make it
-works, use "patch -p0 < dev/doc/patch.ocaml-3.10.drop.rectypes" to
-hack script/coqmktop.ml, then recompile coqtop.byte. The procedure
-above then works as soon as coqtop.byte is called with at least one
-argument (add neutral option -byte to ensure at least one argument).
-
-
 Debugging from Caml debugger
 ============================
 
diff --git a/dev/doc/patch.ocaml-3.10.drop.rectypes b/dev/doc/patch.ocaml-3.10.drop.rectypes
deleted file mode 100644
index ba7a3e9504..0000000000
--- a/dev/doc/patch.ocaml-3.10.drop.rectypes
+++ /dev/null
@@ -1,31 +0,0 @@
-Index: scripts/coqmktop.ml
-===================================================================
---- scripts/coqmktop.ml	(révision 12084)
-+++ scripts/coqmktop.ml	(copie de travail)
-@@ -231,12 +231,25 @@
-      end;;
- 
-      let ppf = Format.std_formatter;;
-+     let set_rectypes_hack () =
-+       if String.length (Sys.ocaml_version) >= 4 &
-+          String.sub (Sys.ocaml_version) 0 4 = \"3.10\"
-+       then
-+         (* ocaml 3.10 does not have #rectypes but needs it *)
-+         (* simulate a call with option -rectypes before *)
-+         (* jumping to the ocaml toplevel *)
-+         for i = 1 to Array.length Sys.argv - 1 do
-+           Sys.argv.(i) <- \"-rectypes\"
-+         done
-+       else
-+         () in
-+
-      Mltop.set_top
-        {Mltop.load_obj=
-          (fun f -> if not (Topdirs.load_file ppf f) then failwith \"error\");
-         Mltop.use_file=Topdirs.dir_use ppf;
-         Mltop.add_dir=Topdirs.dir_directory;
--        Mltop.ml_loop=(fun () -> Toploop.loop ppf) };;\n"
-+        Mltop.ml_loop=(fun () -> set_rectypes_hack(); Topmain.main()) };;\n"
- 
- (* create a temporary main file to link *)
- let create_tmp_main_file modules =
diff --git a/myocamlbuild.ml b/myocamlbuild.ml
index d6042b7c31..5f838571d8 100644
--- a/myocamlbuild.ml
+++ b/myocamlbuild.ml
@@ -320,13 +320,14 @@ let extra_rules () = begin
        Cmd (S [!Options.ocamlc; A"-c"; A"-pp";
 	       Quote (S [camlp4o; T(tags_of_pathname ml4 ++ "p4mod");
 			 A"-DByte";A"-DHasDynlink";camlp4compat;A"-impl"]);
-	       A"-rectypes"; camlp4incl; incl ml4; A"-impl"; P ml4]));
+	       camlp4incl; incl ml4; A"-impl"; P ml4]));
 
-(** All caml files are compiled with -rectypes and +camlp4/5
+(** All caml files are compiled with +camlp4/5
     and ide files need +lablgtk2 *)
 
-  flag ["compile"; "ocaml"] (S [A"-rectypes"; camlp4incl]);
-  flag ["link"; "ocaml"] (S [A"-rectypes"; camlp4incl]);
+  flag ["compile"; "ocaml"; "rectypes" ] (A "-rectypes");
+  flag ["compile"; "ocaml"] camlp4incl;
+  flag ["link"; "ocaml"] camlp4incl;
   flag ["ocaml"; "ide"; "compile"] lablgtkincl;
   flag ["ocaml"; "ide"; "link"] lablgtkincl;
   flag ["ocaml"; "ide"; "link"; "byte"]
diff --git a/scripts/coqmktop.ml b/scripts/coqmktop.ml
index 60dfeb28d6..503d05883a 100644
--- a/scripts/coqmktop.ml
+++ b/scripts/coqmktop.ml
@@ -220,18 +220,7 @@ let tmp_dynlink()=
 let declare_loading_string () =
   if not !top then
     "Mltop.remove ();;"
-  else
-    "begin try\
-\n       (* Enable rectypes in the toplevel if it has the directive #rectypes *)\
-\n       begin match Hashtbl.find Toploop.directive_table \"rectypes\" with\
-\n         | Toploop.Directive_none f -> f ()\
-\n         | _ -> ()\
-\n       end\
-\n     with\
-\n       | Not_found -> ()\
-\n     end;;\
-\n\
-\n     let ppf = Format.std_formatter;;\
+  else "let ppf = Format.std_formatter;;\
 \n     Mltop.set_top\
 \n       {Mltop.load_obj=\
 \n         (fun f -> if not (Topdirs.load_file ppf f) then Errors.error (\"Could not load plugin \"^f));\
@@ -297,7 +286,7 @@ let main () =
       (* add topstart.cmo explicitly because we shunted ocamlmktop wrapper *)
     let args = if !top then args @ [ "topstart.cmo" ] else args in
       (* Now, with the .cma, we MUST use the -linkall option *)
-    let command = String.concat " " (prog::"-rectypes"::args) in
+    let command = String.concat " " (prog::args) in
       if !echo then
 	begin
 	  print_endline command;
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index 3b2c63b0fa..88ffb14ab0 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -410,10 +410,10 @@ let variables is_install opt (args,defs) =
     List.iter (fun c -> print " \\
   -I $(COQLIB)/"; print c) Coq_config.plugins_dirs; print "\n";
     print "ZFLAGS=$(OCAMLLIBS) $(COQSRCLIBS) -I $(CAMLP4LIB)\n\n";
-    print "CAMLC?=$(OCAMLC) -c -rectypes\n";
-    print "CAMLOPTC?=$(OCAMLOPT) -c -rectypes\n";
-    print "CAMLLINK?=$(OCAMLC) -rectypes\n";
-    print "CAMLOPTLINK?=$(OCAMLOPT) -rectypes\n";
+    print "CAMLC?=$(OCAMLC) -c\n";
+    print "CAMLOPTC?=$(OCAMLOPT) -c\n";
+    print "CAMLLINK?=$(OCAMLC)\n";
+    print "CAMLOPTLINK?=$(OCAMLOPT)\n";
     print "GRAMMARS?=grammar.cma\n";
     print "ifeq ($(CAMLP4),camlp5)
 CAMLP4EXTEND=pa_extend.cmo q_MLast.cmo pa_macro.cmo
@@ -604,9 +604,9 @@ let main_targets vfiles (mlifiles,ml4files,mlfiles,mllibfiles,mlpackfiles) other
     begin
       print "mlihtml: $(MLIFILES:.mli=.cmi)\n";
       print "\t mkdir $@ || rm -rf $@/*\n";
-      print "\t$(OCAMLDOC) -html -rectypes -d $@ -m A $(ZDEBUG) $(ZFLAGS) $(^:.cmi=.mli)\n\n";
+      print "\t$(OCAMLDOC) -html -d $@ -m A $(ZDEBUG) $(ZFLAGS) $(^:.cmi=.mli)\n\n";
       print "all-mli.tex: $(MLIFILES:.mli=.cmi)\n";
-      print "\t$(OCAMLDOC) -latex -rectypes -o $@ -m A $(ZDEBUG) $(ZFLAGS) $(^:.cmi=.mli)\n\n";
+      print "\t$(OCAMLDOC) -latex -o $@ -m A $(ZDEBUG) $(ZFLAGS) $(^:.cmi=.mli)\n\n";
     end;
   if !some_vfile then
     begin