diff options
Diffstat (limited to 'pretyping/detyping.ml')
| -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 |