diff options
| author | Jim Fehrle | 2020-10-11 18:39:16 -0700 |
|---|---|---|
| committer | Jim Fehrle | 2020-10-27 12:15:35 -0700 |
| commit | b402adc12c00ba72046423d3a1737ccad517f70e (patch) | |
| tree | 1940efc064bf87b9b996a0e21eaa75e9b57605d4 /test-suite/misc/quotation_token/src | |
| parent | 5f5cddae48c08872107f30938dcc2f3c8d91f33a (diff) | |
Rename operconstr -> term
Diffstat (limited to 'test-suite/misc/quotation_token/src')
| -rw-r--r-- | test-suite/misc/quotation_token/src/quotation.mlg | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/test-suite/misc/quotation_token/src/quotation.mlg b/test-suite/misc/quotation_token/src/quotation.mlg index 961b170a0d..ba0bcb1b3c 100644 --- a/test-suite/misc/quotation_token/src/quotation.mlg +++ b/test-suite/misc/quotation_token/src/quotation.mlg @@ -2,9 +2,9 @@ open Pcoq.Constr } GRAMMAR EXTEND Gram - GLOBAL: operconstr; + GLOBAL: term; - operconstr: LEVEL "0" + term: LEVEL "0" [ [ s = QUOTATION "foobar:" -> { CAst.make ~loc Constrexpr.(CSort Glob_term.(UNamed [GProp,0])) } ] ] |