diff options
| author | Pierre-Marie Pédrot | 2016-11-18 11:49:25 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-11-18 11:53:55 +0100 |
| commit | 80cfb61c8c497a2d33a6b47fcdaa9d071223a502 (patch) | |
| tree | 4371040b97d39647f9e8679e4d8e8a1a6b077a3a /pretyping/evarconv.mli | |
| parent | 0f5e89ec54bc613f59ce971e6a95ed1161ffc37b (diff) | |
| parent | bdcf5b040b975a179fe9b2889fea0d38ae4689df (diff) | |
Merge branch 'v8.6'
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 14947c8927..2231e5bc30 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 *) |