aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/coqtop.ml
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/coqtop.ml')
-rw-r--r--toplevel/coqtop.ml6
1 files changed, 5 insertions, 1 deletions
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 4ee405318..130271aef 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -166,7 +166,11 @@ let parse_args is_ide =
| "-compile-verbose" :: [] -> usage ()
| "-translate" :: rem -> make_translate true; parse rem
- | "-ftranslate" :: rem -> make_translate true; translate_file := true; parse rem
+ | "-ftranslate" :: rem ->
+ make_translate true;
+ translate_file := true;
+ Constrextern.print_coercions := true;
+ parse rem
| "-unsafe" :: f :: rem -> add_unsafe f; parse rem
| "-unsafe" :: [] -> usage ()