From b47498df42e23b99887a8df616d236029b839337 Mon Sep 17 00:00:00 2001
From: gareuselesinge
Date: Wed, 7 Nov 2012 18:22:13 +0000
Subject: Fix reference_or_constr grammar rule to accept @t as a constr

With the previous formulation extra parentheses had to be added,
now they are only necessary for compound expressions, like an
application.

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

diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index 24efbcc5ef..194ed59262 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -102,7 +102,7 @@ GEXTEND Gram
   ;
   reference_or_constr:
    [ [ r = global -> HintsReference r
-     | "("; c = operconstr LEVEL "200"; ")" -> HintsConstr c ] ]
+     | c = constr -> HintsConstr c ] ]
   ;
   hint:
     [ [ IDENT "Resolve"; lc = LIST1 reference_or_constr; n = OPT natural ->
-- 
cgit v1.2.3