diff options
| author | Hugo Herbelin | 2020-02-02 21:36:14 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-02-11 16:20:36 +0100 |
| commit | 181e9162b40e9ad0bd6afb28d277e36e8912b2e7 (patch) | |
| tree | c2fb979fb03f321c324a1219ca7dee2ddac8f2d3 /interp/constrintern.mli | |
| parent | 18e0103e33b276a88000dde8fccc772af2ca67ea (diff) | |
Fixing some residual bugs of PR #10202 (manual implicit args in subterms).
- Implicit arguments in the return clause and in the branches
of a match were not checked.
- Implicit arguments in each declaration of intern_context were not
restarted.
- Additionally, in intern_context, we take into account ids from the
env on top of which intern_context is called.
- A better approximation of the check for manual implicit in notations
improved (though not fully correct because the exact context of
interpretation of a binder in a notation with recursive binders is
not known).
We also rename impl_binder_index into binder_block_names in anticipation of
checking redundancies also for non-implicit arguments.
Diffstat (limited to 'interp/constrintern.mli')
| -rw-r--r-- | interp/constrintern.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/interp/constrintern.mli b/interp/constrintern.mli index 8cce7cd9af..670563f02f 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -97,7 +97,7 @@ val intern_context : env -> internalization_env -> local_binder_expr list -> int (** 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 -> +val interp_constr : ?expected_type:typing_constraint -> env -> evar_map -> ?impls:internalization_env -> constr_expr -> constr Evd.in_evar_universe_context val interp_casted_constr : env -> evar_map -> ?impls:internalization_env -> @@ -109,7 +109,7 @@ val interp_type : env -> evar_map -> ?impls:internalization_env -> (** 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 : ?expected_type:typing_constraint -> env -> evar_map -> constr_expr -> evar_map * constr (** Accepting unresolved evars *) |