diff options
| author | Pierre-Marie Pédrot | 2015-10-29 13:04:22 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-10-29 13:11:38 +0100 |
| commit | f970991baef49fa5903e6b7aeb6ac62f8cfdf822 (patch) | |
| tree | 0b14bafe702a6219d960111148ff3a0cdc9e18e6 /interp | |
| parent | 4444f04cfdbe449d184ac1ce0a56eb484805364d (diff) | |
| parent | 78378ba9a79b18a658828d7a110414ad18b9a732 (diff) | |
Merge branch 'v8.5'
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 4d2c994679..b671c98815 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 *) |