aboutsummaryrefslogtreecommitdiff
path: root/scripts
diff options
context:
space:
mode:
Diffstat (limited to 'scripts')
-rw-r--r--scripts/coqmktop.ml3
1 files changed, 1 insertions, 2 deletions
diff --git a/scripts/coqmktop.ml b/scripts/coqmktop.ml
index 77f9b0e53b..5d35298e8a 100644
--- a/scripts/coqmktop.ml
+++ b/scripts/coqmktop.ml
@@ -245,8 +245,7 @@ let declare_loading_string () =
else if not !top then
"Mltop.set Mltop.WithoutTop;;\n"
else
- "Clflags.recursive_types:=true;;
- let ppf = Format.std_formatter;;
+ "let ppf = Format.std_formatter;;
Mltop.set (Mltop.WithTop
{Mltop.load_obj=Topdirs.dir_load ppf;
Mltop.use_file=Topdirs.dir_use ppf;