diff options
| -rw-r--r-- | pretyping/retyping.mli | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/pretyping/retyping.mli b/pretyping/retyping.mli index dd0727b032..379a03956b 100644 --- a/pretyping/retyping.mli +++ b/pretyping/retyping.mli @@ -20,5 +20,8 @@ val get_type_of : env -> 'a evar_map -> constr -> constr val get_type_of_with_meta : env -> 'a evar_map -> metamap -> constr -> constr val get_sort_of : env -> 'a evar_map -> constr -> sorts -(*Makes an unsafe judgment from a constr*) -val mk_unsafe_judgment:env->'a evar_map->constr ->unsafe_judgment;; +(* Makes an assumption from a constr *) +val get_assumption_of : env -> 'a evar_map -> constr -> typed_type + +(* Makes an unsafe judgment from a constr *) +val get_judgment_of : env -> 'a evar_map -> constr -> unsafe_judgment |