diff options
| author | Benjamin Gregoire | 2015-03-27 06:44:02 +0100 |
|---|---|---|
| committer | Benjamin Gregoire | 2015-03-27 06:46:08 +0100 |
| commit | 924a6e99f85aa0d70d42e753d6901b067ebf8f1d (patch) | |
| tree | bc6d71b35edbd645394aa441722f7a2a14741ec5 /dev | |
| parent | 00894adf6fc11f4336a3ece0c347676bbf0b4c11 (diff) | |
use a more compact representation of non-constant constructors
for which there corresponding tag are greater than max_variant_tag.
The code is a merge with the patch proposed by Bruno on
github barras/coq
commit/504c753d7bb104ff4453fa0ede21c870ae2bb00c
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/vm_printers.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/dev/vm_printers.ml b/dev/vm_printers.ml index a583e2e54e..4578a3b33d 100644 --- a/dev/vm_printers.ml +++ b/dev/vm_printers.ml @@ -74,14 +74,14 @@ and ppwhd whd = | Vfix _ -> print_vfix() | Vcofix _ -> print_string "cofix" | Vconstr_const i -> print_string "C(";print_int i;print_string")" - | Vconstr_block (tag,b) -> ppvblock tag b + | Vconstr_block b -> ppvblock b | Vatom_stk(a,s) -> open_hbox();ppatom a;close_box(); print_string"@";ppstack s -and ppvblock tag b = +and ppvblock b = open_hbox(); - print_string "Cb(";print_int tag; + print_string "Cb(";print_int (btag b); let n = bsize b in for i = 0 to n -1 do print_string ",";ppvalues (bfield b i) |