Skip to content

Commit

Permalink
Merge pull request #117 from SkySkimmer/constrextern-max-depth
Browse files Browse the repository at this point in the history
Adapt to coq/coq#20275 (Printing Depth has effect at extern time)
  • Loading branch information
ppedrot authored Mar 6, 2025
2 parents 2b50da7 + feab74c commit c33eae9
Show file tree
Hide file tree
Showing 2 changed files with 1 addition and 0 deletions.
Binary file modified test-suite/output/BinaryPrintingNotations.v
Binary file not shown.
1 change: 1 addition & 0 deletions test-suite/output/allBytes.v
Original file line number Diff line number Diff line change
Expand Up @@ -117,6 +117,7 @@ Notation "'}'" := (Byte.x7d) (only printing).
Notation "'~'" := (Byte.x7e) (only printing, at level 0).

Global Set Printing Width 300.
Set Printing Depth 100.

Goal False.
let cc := eval cbv in allBytes in idtac cc.
Expand Down

0 comments on commit c33eae9

Please sign in to comment.