From 140432ecdfce056c8e2b4271081a13af5dd603a9 Mon Sep 17 00:00:00 2001
From: herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Fri, 11 Apr 2003 19:04:24 +0000
Subject: Ajout option 'Local' à Infix et Notation
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3916 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 toplevel/command.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'toplevel/command.ml')

diff --git a/toplevel/command.ml b/toplevel/command.ml
index 6c33b3783..ed77973c2 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -122,7 +122,7 @@ let declare_definition ident local bl red_option c typopt =
 let syntax_definition ident c =
   let c = snd (interp_aconstr [] c) in 
   let onlyparse = !Options.v7_only in
-  Syntax_def.declare_syntactic_definition ident onlyparse c;
+  Syntax_def.declare_syntactic_definition false ident onlyparse c;
   if_verbose message ((string_of_id ident) ^ " is now a syntax macro")
 
 
-- 
cgit v1.2.3