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 /toplevel/command.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 'toplevel/command.ml')
| -rw-r--r-- | toplevel/command.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/command.ml b/toplevel/command.ml index 12c387dcf3..7ffe680e5e 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -1129,7 +1129,7 @@ let interp_recursive isfix fixl notations = () in (* Instantiate evars and check all are resolved *) - let evd = consider_remaining_unif_problems env_rec !evdref in + let evd = solve_unif_constraints_with_heuristics env_rec !evdref in let evd, nf = nf_evars_and_universes evd in let fixdefs = List.map (Option.map nf) fixdefs in let fixtypes = List.map nf fixtypes in |