diff options
Diffstat (limited to 'pretyping/pretyping.ml')
| -rw-r--r-- | pretyping/pretyping.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 0cadffa4f..03fe2122c 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -374,7 +374,7 @@ let pretype_ref loc evdref env ref us = | ref -> let evd, c = pretype_global loc univ_flexible env !evdref ref us in let () = evdref := evd in - let ty = Typing.type_of env evd c in + let ty = Typing.unsafe_type_of env evd c in make_judge c ty let judge_of_Type evd s = |