Nouvelle mouture du traducteur v7->v8

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

1 files changed, 3 insertions, 1 deletions

diff --git a/library/impargs.ml b/library/impargs.ml
index 38267c3c8e..e35cf03165 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -32,7 +32,9 @@ let contextual_implicit_args_out = ref false
 
 let make_implicit_args flag =
   implicit_args := flag;
-  if not !Options.v7_only then implicit_args_out := flag
+  if not !Options.v7_only then implicit_args_out := flag;
+  if !Options.translate_strict_impargs then
+    strict_implicit_args_out := not flag
 
 let make_strict_implicit_args flag =
   strict_implicit_args := flag;