From 62ce65dadb0afb8815b26069246832662846c7ec Mon Sep 17 00:00:00 2001
From: mdenes
Date: Tue, 22 Jan 2013 14:18:38 +0000
Subject: Revert "remove -rectypes except for term.ml"

Preparing landing of the native compiler, which requires -rectypes flag.

This reverts commit f975575187d0a19e7cc1afc43459a92eeb12b3f1.



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16135 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 dev/doc/debugging.txt | 9 +++++++++
 1 file changed, 9 insertions(+)

(limited to 'dev/doc/debugging.txt')

diff --git a/dev/doc/debugging.txt b/dev/doc/debugging.txt
index 83512c658b..2480b8edb3 100644
--- a/dev/doc/debugging.txt
+++ b/dev/doc/debugging.txt
@@ -21,6 +21,15 @@ 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
 ============================
 
-- 
cgit v1.2.3