diff options
| -rw-r--r-- | parsing/g_proofs.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
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 -> |