From 67a624a8b9e0dfac95cc86134f05cc247cfa179c Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 17 Dec 2012 17:53:14 +0000
Subject: Do not display REVERTcast inserted by reduction tactics (unless
 printing all). Question of printing DEFAULTcast inserted by reduction tactics
 still open.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16081 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/detyping.ml | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index af8cc43c17..001f3b5a67 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -396,6 +396,8 @@ let rec detype (isgoal:bool) avoid env t =
 	 with _ ->
 	  GVar (dl, id))
     | Sort s -> GSort (dl,detype_sort s)
+    | Cast (c1,REVERTcast,c2) when not !Flags.raw_print ->
+        detype isgoal avoid env c1
     | Cast (c1,k,c2) ->
         let d1 = detype isgoal avoid env c1 in
 	let d2 = detype isgoal avoid env c2 in
-- 
cgit v1.2.3