From 8677ac9dce9a617755eae07c19f0b1f42ad6af55 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 12 Sep 2003 19:33:17 +0000
Subject: Un seul binaire commun v7 et v8 avec détection précoce de l'option
 -v8 et choix du parseur en fonction de cette option

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

(limited to 'library')

diff --git a/library/impargs.ml b/library/impargs.ml
index e35cf03165..224d1cc769 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -22,8 +22,9 @@ open Nametab
 
 (*s Flags governing the computation of implicit arguments *)
 
+(* les implicites sont stricts par défaut en v8 *)
 let implicit_args = ref false
-let strict_implicit_args = ref false
+let strict_implicit_args = ref (not !Options.v7)
 let contextual_implicit_args = ref false
 
 let implicit_args_out = ref false
@@ -485,7 +486,7 @@ let _ =
 let init () =
   (* strict_implicit_args_out must be not !Options.v7 
      but init is done before parsing *)
-  strict_implicit_args:=false;
+  strict_implicit_args:=not !Options.v7;
   implicit_args_out:=false;
   (* strict_implicit_args_out needs to be not !Options.v7 or
      Options.do_translate() but init is done before parsing *)
-- 
cgit v1.2.3