diff options
Diffstat (limited to 'parsing')
| -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 33f375a839..fe8e0787c3 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -81,7 +81,7 @@ GEXTEND Gram | IDENT "Stm"; IDENT "JoinDocument"; "." -> VernacStm JoinDocument | IDENT "Stm"; IDENT "Finish"; "." -> VernacStm Finish | IDENT "Stm"; IDENT "Observe"; id = INT; "." -> - VernacStm (Observe (Stateid.state_id_of_int (int_of_string id))) + VernacStm (Observe (Stateid.of_int (int_of_string id))) | IDENT "Stm"; IDENT "Command"; v = vernac_aux -> VernacStm (Command v) | IDENT "Stm"; IDENT "PGLast"; v = vernac_aux -> VernacStm (PGLast v) |