From 9ee004e00a0b5ef2bb86c1cd201382ab30673d8f Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 21 Sep 2003 22:56:01 +0000
Subject: Renommage Implicits -> Implicit

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4436 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 toplevel/vernacentries.ml | 10 ++++++----
 1 file changed, 6 insertions(+), 4 deletions(-)

diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index f21a9c57e8..e4a432d468 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -741,11 +741,13 @@ let _ =
       optread  = Impargs.is_implicit_args;
       optwrite = Impargs.make_implicit_args }
 
+let impargs = if !Options.v7 then "Implicits" else "Implicit"
+
 let _ =
   declare_bool_option 
     { optsync  = false; (* synchronisation is in Impargs *)
       optname  = "strict implicits";
-      optkey   = (SecondaryTable ("Strict","Implicits"));
+      optkey   = (SecondaryTable ("Strict",impargs));
       optread  = Impargs.is_strict_implicit_args;
       optwrite = Impargs.make_strict_implicit_args }
 
@@ -753,7 +755,7 @@ let _ =
   declare_bool_option 
     { optsync  = true;
       optname  = "contextual implicits";
-      optkey   = (SecondaryTable ("Contextual","Implicits"));
+      optkey   = (SecondaryTable ("Contextual",impargs));
       optread  = Impargs.is_contextual_implicit_args;
       optwrite = Impargs.make_contextual_implicit_args }
 
@@ -769,7 +771,7 @@ let _ =
   declare_bool_option 
     { optsync  = true;
       optname  = "implicits printing";
-      optkey   = (SecondaryTable ("Printing","Implicits"));
+      optkey   = (SecondaryTable ("Printing",impargs));
       optread  = (fun () -> !Constrextern.print_implicits);
       optwrite = (fun b ->  Constrextern.print_implicits := b) }
 
@@ -777,7 +779,7 @@ let _ =
   declare_bool_option 
     { optsync  = true;
       optname  = "symbols printing";
-      optkey   = (SecondaryTable ("Printing","Symbols"));
+      optkey   = (SecondaryTable ("Printing",if !Options.v7 then "Symbols" else "Notations"));
       optread  = (fun () -> not !Constrextern.print_no_symbol);
       optwrite = (fun b ->  Constrextern.print_no_symbol := not b) }
 
-- 
cgit v1.2.3