From 9c3f02a3a1f3e7ca96c5de44f3d4142268c9d96c Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 22 Sep 2003 17:09:15 +0000
Subject: Anglais

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

diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index e4a432d468..de9db0a818 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -746,7 +746,7 @@ let impargs = if !Options.v7 then "Implicits" else "Implicit"
 let _ =
   declare_bool_option 
     { optsync  = false; (* synchronisation is in Impargs *)
-      optname  = "strict implicits";
+      optname  = "strict implicit arguments";
       optkey   = (SecondaryTable ("Strict",impargs));
       optread  = Impargs.is_strict_implicit_args;
       optwrite = Impargs.make_strict_implicit_args }
@@ -754,7 +754,7 @@ let _ =
 let _ =
   declare_bool_option 
     { optsync  = true;
-      optname  = "contextual implicits";
+      optname  = "contextual implicit arguments";
       optkey   = (SecondaryTable ("Contextual",impargs));
       optread  = Impargs.is_contextual_implicit_args;
       optwrite = Impargs.make_contextual_implicit_args }
@@ -770,7 +770,7 @@ let _ =
 let _ =
   declare_bool_option 
     { optsync  = true;
-      optname  = "implicits printing";
+      optname  = "implicit arguments printing";
       optkey   = (SecondaryTable ("Printing",impargs));
       optread  = (fun () -> !Constrextern.print_implicits);
       optwrite = (fun b ->  Constrextern.print_implicits := b) }
-- 
cgit v1.2.3