diff options
Diffstat (limited to 'test-suite/misc/quotation_token/src')
| -rw-r--r-- | test-suite/misc/quotation_token/src/quotation.mlg | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/misc/quotation_token/src/quotation.mlg b/test-suite/misc/quotation_token/src/quotation.mlg index ba0bcb1b3c..0f843b3b14 100644 --- a/test-suite/misc/quotation_token/src/quotation.mlg +++ b/test-suite/misc/quotation_token/src/quotation.mlg @@ -7,6 +7,6 @@ GRAMMAR EXTEND Gram term: LEVEL "0" [ [ s = QUOTATION "foobar:" -> { - CAst.make ~loc Constrexpr.(CSort Glob_term.(UNamed [GProp,0])) } ] ] + CAst.make ~loc Constrexpr.(CSort Glob_term.(UNamed [CProp,0])) } ] ] ; END |