diff options
| author |  Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2018-02-20 16:03:57 +0100 |
|---|---|---|
| committer | Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2018-03-02 23:45:51 +0100 |
| commit | 3ce123f16ce19f67dde4a0f3f2874a2678649907 (patch) | |
| tree | 1357c6556ba947f066c16a1aa946c7e2ddb399d4 /pretyping/unification.ml | |
| parent | a4817d25befc71b7dbf707637660431144985133 (diff) | |
Remove 8.5 compatibility support.
Diffstat (limited to 'pretyping/unification.ml')
| -rw-r--r-- | pretyping/unification.ml | 7 |
1 files changed, 1 insertions, 6 deletions
diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 48d8a372c..6106b6ef6 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -1304,12 +1304,7 @@ let solve_simple_evar_eqn ts env evd ev rhs = match solve_simple_eqn (Evarconv.evar_conv_x ts) env evd (None,ev,rhs) with | UnifFailure (evd,reason) -> error_cannot_unify env evd ~reason (mkEvar ev,rhs); - | Success evd -> - if Flags.version_less_or_equal Flags.V8_5 then - (* We used to force solving unrelated problems at arbitrary times *) - Evarconv.solve_unif_constraints_with_heuristics env evd - else (* solve_simple_eqn calls reconsider_unif_constraints itself *) - evd + | Success evd -> evd (* [w_merge env sigma b metas evars] merges common instances in metas or in evars, possibly generating new unification problems; if [b] |