diff options
Diffstat (limited to 'parsing/g_proofs.ml4')
| -rw-r--r-- | parsing/g_proofs.ml4 | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4 index dfb59a19d..aef2f05eb 100644 --- a/parsing/g_proofs.ml4 +++ b/parsing/g_proofs.ml4 @@ -15,6 +15,7 @@ open Topconstr open Vernacexpr open Prim open Constr +open Tok let thm_token = G_vernac.thm_token @@ -29,7 +30,7 @@ GEXTEND Gram ; opt_hintbases: [ [ -> [] - | ":"; l = LIST1 IDENT -> l ] ] + | ":"; l = LIST1 [id = IDENT -> id ] -> l ] ] ; command: [ [ IDENT "Goal"; c = lconstr -> VernacGoal c |