diff options
Diffstat (limited to 'contrib/correctness/psyntax.ml4')
| -rw-r--r-- | contrib/correctness/psyntax.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/correctness/psyntax.ml4 b/contrib/correctness/psyntax.ml4 index 5e0f9ad42..fc09cfa69 100644 --- a/contrib/correctness/psyntax.ml4 +++ b/contrib/correctness/psyntax.ml4 @@ -561,7 +561,7 @@ open Vernac GEXTEND Gram Pcoq.Vernac_.vernac: [ [ IDENT "Global"; "Variable"; - l = LIST1 IDENT SEP ","; ":"; t = type_v; "." -> + l = LIST1 ident SEP ","; ":"; t = type_v; "." -> let idl = List.map Ast.nvar l in let d = Ast.dynamic (in_typev t) in <:ast< (PROGVARIABLE (VERNACARGLIST ($LIST $idl)) (VERNACDYN $d)) >> |