From a638cba857c9a93a62f35bcceab6fa2c710805d2 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 25 Sep 2011 18:07:06 +0000
Subject: Polishing commits r14492, r14448 and r14407 (tactics propagate
 conversion hints to kernel). Whether REVERTcast must be known from coqchk is
 unclear. In the meantime, warn about the unstability of the situation (see
 also bug #2599).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14495 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 dev/top_printers.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'dev')

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
-- 
cgit v1.2.3