diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-10-24 18:10:24 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-10-26 20:05:41 +0100 |
| commit | d1114c5f55fcb96a99a1a5562b014414ad8217ba (patch) | |
| tree | c5efe18fb5ab4006ffab90f7db7d878556a14398 /interp | |
| parent | d4edd135e7cb8b6f86d9d5a0d320e0b29ee20148 (diff) | |
Documenting a bit more interpretation functions in passing.
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrintern.mli | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/interp/constrintern.mli b/interp/constrintern.mli index 4d2c99467..b671c9881 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -95,7 +95,8 @@ val intern_context : bool -> env -> internalization_env -> local_binder list -> (** {6 Composing internalization with type inference (pretyping) } *) -(** Main interpretation functions expecting evars to be all resolved *) +(** Main interpretation functions, using type class inference, + expecting evars and pending problems to be all resolved *) val interp_constr : env -> evar_map -> ?impls:internalization_env -> constr_expr -> constr Evd.in_evar_universe_context @@ -106,9 +107,10 @@ val interp_casted_constr : env -> evar_map -> ?impls:internalization_env -> val interp_type : env -> evar_map -> ?impls:internalization_env -> constr_expr -> types Evd.in_evar_universe_context -(** Main interpretation function expecting evars to be all resolved *) +(** Main interpretation function expecting all postponed problems to + be resolved, but possibly leaving evars. *) -val interp_open_constr : env -> evar_map -> constr_expr -> evar_map * constr +val interp_open_constr : env -> evar_map -> constr_expr -> evar_map * constr (** Accepting unresolved evars *) |