From d1cd53c161f8534a6756b92ca3072155b726f531 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 11 Aug 2003 10:23:28 +0000
Subject: Nouvelle mouture du traducteur v7->v8

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4255 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 library/impargs.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

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;
-- 
cgit v1.2.3