diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-09-04 10:23:28 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-09-04 15:22:27 +0200 |
| commit | 3806d567af6b1feee2c8f196199eee4208a8551d (patch) | |
| tree | 5e6a7657058d52f18869c3bdfa618e5f7bb26b90 /pretyping/typing.mli | |
| parent | f3b714f5a8e516ee9731d705808a4084caae5a1e (diff) | |
Typing.sort_of does not leak evarmaps anymore.
Diffstat (limited to 'pretyping/typing.mli')
| -rw-r--r-- | pretyping/typing.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/typing.mli b/pretyping/typing.mli index 03e62e006..8700df52a 100644 --- a/pretyping/typing.mli +++ b/pretyping/typing.mli @@ -22,7 +22,7 @@ val type_of : env -> evar_map -> constr -> types val e_type_of : ?refresh:bool -> env -> evar_map -> constr -> evar_map * types (** Typecheck a type and return its sort *) -val sort_of : env -> evar_map -> types -> sorts +val sort_of : env -> evar_map ref -> types -> sorts (** Typecheck a term has a given type (assuming the type is OK) *) val check : env -> evar_map -> constr -> types -> unit |