diff options
| -rw-r--r-- | parsing/g_vernac.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 03b1466481..7f4a995424 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -220,7 +220,7 @@ GEXTEND Gram | "CoInductive" -> (CoInductive,CoFinite) ] ] ; infer_token: - [ [ "Infer" -> true | -> false ] ] + [ [ IDENT "Infer" -> true | -> false ] ] ; record_token: [ [ IDENT "Record" -> (Record,BiFinite) |