diff options
Diffstat (limited to 'pretyping/detyping.ml')
| -rw-r--r-- | pretyping/detyping.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 1adda14ab..84022f57f 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -457,7 +457,7 @@ let rec detype flags avoid env sigma t = | Var id -> (try let _ = Global.lookup_named id in GRef (dl, VarRef id, None) with Not_found -> GVar (dl, id)) - | Sort s -> GSort (dl,detype_sort sigma s) + | Sort s -> GSort (dl,detype_sort sigma (ESorts.kind sigma s)) | Cast (c1,REVERTcast,c2) when not !Flags.raw_print -> detype flags avoid env sigma c1 | Cast (c1,k,c2) -> |