Merge PR #14836: [CI failure] Fix bad interaction between merging of #…

…13664 and #14598 Reviewed-by: ppedrot
coq · Sep 2, 2021 · 6685a40 · 6685a40
2 parents 6bd07ba + e63ee29
commit 6685a40
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/test-suite/output/PrintGrammarConstr.out b/test-suite/output/PrintGrammarConstr.out
@@ -45,8 +45,8 @@ and term is
 | "8" LEFTA
   [  ]
 | "1" LEFTA
-  [ SELF; ".("; "@"; global; LIST0 (term LEVEL "9"); ")"
-  | SELF; ".("; global; LIST0 arg; ")"
+  [ SELF; ".("; "@"; global; univ_annot; LIST0 (term LEVEL "9"); ")"
+  | SELF; ".("; global; univ_annot; LIST0 arg; ")"
   | SELF; "%"; IDENT ]
 | "0" LEFTA
   [ "["; term LEVEL "10"; "+"; "+"; "*"; LIST1 (term LEVEL "10") SEP ["+";