diff options
| author | herbelin | 2012-12-17 17:53:14 +0000 |
|---|---|---|
| committer | herbelin | 2012-12-17 17:53:14 +0000 |
| commit | 67a624a8b9e0dfac95cc86134f05cc247cfa179c (patch) | |
| tree | 770ed1356b477ffc533aa62d5f606d25f7df9279 | |
| parent | d09a4df287a125162601e5970bb19aa278be91d6 (diff) | |
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
| -rw-r--r-- | pretyping/detyping.ml | 2 |
1 files changed, 2 insertions, 0 deletions
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 |