diff options
| author | Maxime Dénès | 2020-07-03 10:11:22 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2020-07-03 10:11:22 +0200 |
| commit | 33581635d3ad525e1d5c2fb2587be345a7e77009 (patch) | |
| tree | 1aff9ab6c08d8aa1cee6987875ffbe010ebbc74a /dev/top_printers.ml | |
| parent | ce500b3483bbc80ee8baee3b255c3b09b5b2b17e (diff) | |
| parent | 0c6c495b92186ee357eb6b6a5ff62826040f549c (diff) | |
Merge PR #10390: UIP in SProp
Reviewed-by: Zimmi48
Ack-by: ejgallego
Reviewed-by: maximedenes
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 34110f96cf..3df6f986ce 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -296,7 +296,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)) -> @@ -408,7 +408,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"; |