diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2016-10-22 11:03:13 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2016-10-22 11:32:12 +0200 |
| commit | be11ab322fa73804118738e7a08e9910fdf4600d (patch) | |
| tree | 33373d0bb32d4e46a10556a5b53436fb884f337c /pretyping/evarconv.mli | |
| parent | c9f8f7fe182decedda2e6403d502fda3aff24a6e (diff) | |
Renamings to avoid confusion deprecating old names
reconsider_conv_pbs -> reconsider_unif_constraints
consider_remaining_unif_problems -> solve_unif_constraints_with_heuristics
Diffstat (limited to 'pretyping/evarconv.mli')
| -rw-r--r-- | pretyping/evarconv.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli index 14947c892..2231e5bc3 100644 --- a/pretyping/evarconv.mli +++ b/pretyping/evarconv.mli @@ -33,7 +33,10 @@ val e_cumul : env -> ?ts:transparent_state -> evar_map ref -> constr -> constr - (** Try heuristics to solve pending unification problems and to solve evars with candidates *) +val solve_unif_constraints_with_heuristics : env -> ?ts:transparent_state -> evar_map -> evar_map + val consider_remaining_unif_problems : env -> ?ts:transparent_state -> evar_map -> evar_map +(** @deprecated Alias for [solve_unif_constraints_with_heuristics] *) (** Check all pending unification problems are solved and raise an error otherwise *) |