Skip to content

Commit c33eae9

Browse files
authored
Merge pull request #117 from SkySkimmer/constrextern-max-depth
Adapt to rocq-prover/rocq#20275 (Printing Depth has effect at extern time)
2 parents 2b50da7 + feab74c commit c33eae9

File tree

2 files changed

+1
-0
lines changed

2 files changed

+1
-0
lines changed
25 Bytes
Binary file not shown.

test-suite/output/allBytes.v

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -117,6 +117,7 @@ Notation "'}'" := (Byte.x7d) (only printing).
117117
Notation "'~'" := (Byte.x7e) (only printing, at level 0).
118118

119119
Global Set Printing Width 300.
120+
Set Printing Depth 100.
120121

121122
Goal False.
122123
let cc := eval cbv in allBytes in idtac cc.

0 commit comments

Comments
 (0)