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/evarsolve.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 'pretyping/evarsolve.ml')
| -rw-r--r-- | pretyping/evarsolve.ml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index f1526facc..f0aa9b564 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -1603,7 +1603,7 @@ let status_changed lev (pbty,_,t1,t2) = (try Evar.Set.mem (head_evar t1) lev with NoHeadEvar -> false) || (try Evar.Set.mem (head_evar t2) lev with NoHeadEvar -> false) -let reconsider_conv_pbs conv_algo evd = +let reconsider_unif_constraints conv_algo evd = let (evd,pbs) = extract_changed_conv_pbs evd status_changed in List.fold_left (fun p (pbty,env,t1,t2 as x) -> @@ -1616,6 +1616,8 @@ let reconsider_conv_pbs conv_algo evd = (Success evd) pbs +let reconsider_conv_pbs = reconsider_unif_constraints + (* Tries to solve problem t1 = t2. * Precondition: t1 is an uninstantiated evar * Returns an optional list of evars that were instantiated, or None @@ -1626,7 +1628,7 @@ let solve_simple_eqn conv_algo ?(choose=false) env evd (pbty,(evk1,args1 as ev1) try let t2 = whd_betaiota evd t2 in (* includes whd_evar *) let evd = evar_define conv_algo ~choose env evd pbty ev1 t2 in - reconsider_conv_pbs conv_algo evd + reconsider_unif_constraints conv_algo evd with | NotInvertibleUsingOurAlgorithm t -> UnifFailure (evd,NotClean (ev1,env,t)) |