diff options
Diffstat (limited to 'pretyping/evarconv.ml')
| -rw-r--r-- | pretyping/evarconv.ml | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index d06009dce..a2ffe12e9 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -1089,7 +1089,7 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs = match evar_conv_x ts env_evar evd CUMUL idty evty with | UnifFailure _ -> error "Cannot find an instance" | Success evd -> - match reconsider_conv_pbs (evar_conv_x ts) evd with + match reconsider_unif_constraints (evar_conv_x ts) evd with | UnifFailure _ -> error "Cannot find an instance" | Success evd -> evd @@ -1221,7 +1221,7 @@ let rec solve_unconstrained_evars_with_candidates ts evd = let conv_algo = evar_conv_x ts in let evd = check_evar_instance evd evk a conv_algo in let evd = Evd.define evk a evd in - match reconsider_conv_pbs conv_algo evd with + match reconsider_unif_constraints conv_algo evd with | Success evd -> solve_unconstrained_evars_with_candidates ts evd | UnifFailure _ -> aux l with @@ -1244,7 +1244,7 @@ let solve_unconstrained_impossible_cases env evd = Evd.define evk ty evd' | _ -> evd') evd evd -let consider_remaining_unif_problems env +let solve_unif_constraints_with_heuristics env ?(ts=Conv_oracle.get_transp_state (Environ.oracle env)) evd = let evd = solve_unconstrained_evars_with_candidates ts evd in let rec aux evd pbs progress stuck = @@ -1274,6 +1274,8 @@ let consider_remaining_unif_problems env check_problems_are_solved env heuristic_solved_evd; solve_unconstrained_impossible_cases env heuristic_solved_evd +let consider_remaining_unif_problems = solve_unif_constraints_with_heuristics + (* Main entry points *) exception UnableToUnify of evar_map * unification_error |