From 079f1b21db4b183cd648613ee3e15c4746eb8057 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 11 Aug 2003 10:17:08 +0000
Subject: Nettoyage

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

diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 1f9a08d980..3d11b2412e 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -897,7 +897,6 @@ let add_distfix local assoc n df r sc =
   add_notation_in_scope local df a (Some assoc,n,[],false) None sc (split df)
 
 let add_infix local assoc n inf pr onlyparse mv8 sc =
-(*  let pr = Astterm.globalize_qualid pr in*)
   (* check the precedence *)
   if !Options.v7 & (n<1 or n>10) then
     errorlabstrm "Metasyntax.infix_grammar_entry"
-- 
cgit v1.2.3