aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
Diffstat (limited to 'dev')
-rw-r--r--dev/top_printers.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 278fdb399c..3fc90761d1 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -160,6 +160,7 @@ let cast_kind_display k =
match k with
| VMcast -> "VMcast"
| DEFAULTcast -> "DEFAULTcast"
+ | REVERTcast -> "REVERTcast"
let constr_display csr =
let rec term_display c = match kind_of_term c with