aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel')
-rw-r--r--toplevel/coqtop.ml6
1 files changed, 5 insertions, 1 deletions
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 99c1bed6f..86cbe3654 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -202,7 +202,11 @@ let parse_args is_ide =
| "-v7" :: rem -> Options.v7 := true; parse rem
- | "-v8" :: rem -> Options.v7 := false; parse rem
+ | "-v8" :: rem ->
+ Options.v7 := false;
+ (* implicites stricts par défaut en v8 *)
+ Impargs.make_strict_implicit_args true;
+ parse rem
| s :: rem ->
if is_ide && Filename.check_suffix s ".v" then begin