diff options
Diffstat (limited to 'pretyping/typing.ml')
| -rw-r--r-- | pretyping/typing.ml | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/pretyping/typing.ml b/pretyping/typing.ml index 281e33e9b..5477d804a 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -400,6 +400,11 @@ let e_check env evdref c t = error_actual_type_core env !evdref j t | Some sigma -> evdref := sigma +let check env sigma c t = + let evdref = ref sigma in + e_check env evdref c t; + !evdref + (* Type of a constr *) let unsafe_type_of env evd c = @@ -416,6 +421,11 @@ let e_sort_of env evdref c = let a = e_type_judgment env evdref j in a.utj_type +let sort_of env sigma c = + let evdref = ref sigma in + let a = e_sort_of env evdref c in + !evdref, a + (* Try to solve the existential variables by typing *) let type_of ?(refresh=false) env evd c = |