diff options
| author | Matthieu Sozeau | 2016-10-22 11:03:13 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2016-10-22 11:32:12 +0200 |
| commit | be11ab322fa73804118738e7a08e9910fdf4600d (patch) | |
| tree | 33373d0bb32d4e46a10556a5b53436fb884f337c /proofs/refine.ml | |
| 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 'proofs/refine.ml')
| -rw-r--r-- | proofs/refine.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/proofs/refine.ml b/proofs/refine.ml index 2f21428900..3f55270609 100644 --- a/proofs/refine.ml +++ b/proofs/refine.ml @@ -157,6 +157,6 @@ end } let solve_constraints = let open Proofview in tclENV >>= fun env -> tclEVARMAP >>= fun sigma -> - try let sigma = Evarconv.consider_remaining_unif_problems env sigma in + try let sigma = Evarconv.solve_unif_constraints_with_heuristics env sigma in Unsafe.tclEVARSADVANCE sigma with e -> tclZERO e |