diff options
Diffstat (limited to 'pretyping/retyping.ml')
| -rw-r--r-- | pretyping/retyping.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index 0e61614b3d..6eb095d539 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -15,7 +15,7 @@ type metamap = (int * constr) list let outsort env sigma t = match whd_betadeltaiota env sigma t with DOP0(Sort s) -> s - | _ -> anomaly "outsort: Not a sort" + | _ -> anomaly "Retyping: found a type of type which is not a sort" let rec subst_type env sigma typ = function [] -> typ |