From b402adc12c00ba72046423d3a1737ccad517f70e Mon Sep 17 00:00:00 2001
From: Jim Fehrle
Date: Sun, 11 Oct 2020 18:39:16 -0700
Subject: Rename operconstr -> term

---
 test-suite/misc/quotation_token/src/quotation.mlg | 4 ++--
 test-suite/output/Notations4.out                  | 4 ++--
 2 files changed, 4 insertions(+), 4 deletions(-)

(limited to 'test-suite')

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])) } ] ]
diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out
index a42518822f..fa0c20bf73 100644
--- a/test-suite/output/Notations4.out
+++ b/test-suite/output/Notations4.out
@@ -8,7 +8,7 @@ Entry custom:myconstr is
 | "4" RIGHTA
   [ SELF; "*"; NEXT ]
 | "3" RIGHTA
-  [ "<"; operconstr LEVEL "10"; ">" ] ]
+  [ "<"; term LEVEL "10"; ">" ] ]
 
 [< b > + < b > * < 2 >]
      : nat
@@ -77,7 +77,7 @@ The command has indeed failed with message:
 The format is not the same on the right- and left-hand sides of the special token "..".
 Entry custom:expr is
 [ "201" RIGHTA
-  [ "{"; operconstr LEVEL "200"; "}" ] ]
+  [ "{"; term LEVEL "200"; "}" ] ]
 
 fun x : nat => [ x ]
      : nat -> nat
-- 
cgit v1.2.3