diff options
| author | Gaëtan Gilbert | 2019-06-13 15:39:43 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-07-01 13:06:22 +0200 |
| commit | 2ded4c25e532c5dfca0483c211653768ebed01a7 (patch) | |
| tree | a04b2f787490c8971590e6bdf7dd1ec4220e0290 /dev/top_printers.ml | |
| parent | b017e302f69f20fc4fc3d4088a305194f6c387fa (diff) | |
UIP in SProp
Diffstat (limited to 'dev/top_printers.ml')
| -rw-r--r-- | dev/top_printers.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/dev/top_printers.ml b/dev/top_printers.ml index f14edec639..5becd03bbd 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -294,7 +294,7 @@ let constr_display csr = "MutConstruct(("^(MutInd.to_string sp)^","^(string_of_int i)^")," ^","^(universes_display u)^(string_of_int j)^")" | Proj (p, c) -> "Proj("^(Constant.to_string (Projection.constant p))^","^term_display c ^")" - | Case (ci,p,c,bl) -> + | Case (ci,p,iv,c,bl) -> "MutCase(<abs>,"^(term_display p)^","^(term_display c)^"," ^(array_display bl)^")" | Fix ((t,i),(lna,tl,bl)) -> @@ -406,7 +406,7 @@ let print_pure_constr csr = print_int i; print_string ","; print_int j; print_string ","; universes_display u; print_string ")" - | Case (ci,p,c,bl) -> + | Case (ci,p,iv,c,bl) -> open_vbox 0; print_string "<"; box_display p; print_string ">"; print_cut(); print_string "Case"; |