diff options
Diffstat (limited to 'pretyping/retyping.mli')
| -rw-r--r-- | pretyping/retyping.mli | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/pretyping/retyping.mli b/pretyping/retyping.mli index bb3ffa411..c2a08f4b9 100644 --- a/pretyping/retyping.mli +++ b/pretyping/retyping.mli @@ -35,9 +35,6 @@ val get_sort_of : val get_sort_family_of : ?polyprop:bool -> env -> evar_map -> types -> sorts_family -(** Makes an assumption from a constr *) -val get_assumption_of : env -> evar_map -> constr -> types - (** Makes an unsafe judgment from a constr *) val get_judgment_of : env -> evar_map -> constr -> unsafe_judgment |