Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Fixing one part of coq#5669 (unification heuristics sensitive to choi…
…ce of names). This surprising bug was caused by an Id.Set which was ordering solutions to variable-projection problems in ascii order. We fix it by re-considering the variables involved in the solutions using the declaration order. Note that in practice, this implies preferring a dependent solution over a non-dependent one.
- Loading branch information