From 96aaa2f95ea111a0e9f048e335c25fc74643f280 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 14 May 2004 17:35:08 +0000
Subject: Bug syntaxe AddPath

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5747 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 parsing/g_basevernac.ml4 | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/parsing/g_basevernac.ml4 b/parsing/g_basevernac.ml4
index 6476851637..aab17ff454 100644
--- a/parsing/g_basevernac.ml4
+++ b/parsing/g_basevernac.ml4
@@ -82,9 +82,9 @@ GEXTEND Gram
 	  VernacRemoveLoadPath dir
 
        (* For compatibility *)
-      | IDENT "AddPath"; dir = lstring; "as"; alias = as_dirpath ->
+      | IDENT "AddPath"; dir = lstring; alias = as_dirpath ->
 	  VernacAddLoadPath (false, dir, alias)
-      | IDENT "AddRecPath"; dir = lstring; "as"; alias = as_dirpath ->
+      | IDENT "AddRecPath"; dir = lstring; alias = as_dirpath ->
 	  VernacAddLoadPath (true, dir, alias)
       | IDENT "DelPath"; dir = lstring ->
 	  VernacRemoveLoadPath dir
-- 
cgit v1.2.3