diff options
Diffstat (limited to 'pretyping/pretyping.mli')
| -rw-r--r-- | pretyping/pretyping.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index 2eaa77b822..59e6c00037 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -95,13 +95,13 @@ val understand : ?flags:inference_flags -> ?expected_type:typing_constraint -> [pending], however, it can contain more evars than the pending ones. *) val solve_remaining_evars : ?hook:inference_hook -> inference_flags -> - env -> (* current map *) evar_map -> (* initial map *) evar_map -> evar_map + env -> ?initial:evar_map -> (* current map *) evar_map -> evar_map (** Checking evars and pending conversion problems are all solved, reporting an appropriate error message *) val check_evars_are_solved : - env -> (* current map: *) evar_map -> (* initial map: *) evar_map -> unit + env -> ?initial:evar_map -> (* current map: *) evar_map -> unit (** [check_evars env initial_sigma extended_sigma c] fails if some new unresolved evar remains in [c] *) |