Skip to content

Commit 6549f2f

Browse files
committed
Disable new warnings
1 parent 0fe8fbc commit 6549f2f

2 files changed

Lines changed: 9 additions & 6 deletions

File tree

test-suite/output-coqtop/StrictAssociativity.out

Lines changed: 8 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -19,10 +19,14 @@ Rocq < Identifier 'op12' now a keyword
1919

2020
Rocq < Identifier 'op10' now a keyword
2121

22-
Rocq < Rocq <
23-
Rocq <
24-
Rocq <
25-
Rocq <
22+
Rocq < Rocq < Setting notation at level 0.
23+
24+
Rocq < Setting notation at level 0.
25+
26+
Rocq < Setting notation at level 0.
27+
28+
Rocq < Setting notation at level 0.
29+
2630
Rocq < Rocq < Identifier 'atom3' now a keyword
2731

2832
Rocq < Identifier 'atom2' now a keyword
@@ -656,7 +660,6 @@ Entry simple_tactic is
656660
| IDENT "info_trivial"; auto_using; hintbases
657661
| IDENT "trivial"; auto_using; hintbases
658662
| IDENT "autoapply"; constr; "with"; preident
659-
| IDENT "head_of_constr"; ident; constr
660663
| IDENT "typeclasses"; IDENT "eauto"; IDENT "bfs"; OPT nat_or_var; "with";
661664
LIST1 preident
662665
| IDENT "typeclasses"; IDENT "eauto"; IDENT "bfs"; OPT nat_or_var

test-suite/output-coqtop/StrictAssociativity.v

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
Set Warnings "+level-tolerance".
1+
Set Warnings "+level-tolerance,-closed-notation-not-level-0,-postfix-notation-not-level-1".
22

33
Inductive T := E : T | F : T -> T | G : T -> T -> T.
44
Inductive Parsing {A} := Accept (_ : nat) (_ : A) | Reject (_ : nat) (_ : A).

0 commit comments

Comments
 (0)