Mimer doesn't check existing constraints

[UlfNorell]

Mimer doesn't check existing constraints

[UlfNorell]

No, this is a bigger undertaking that will have to wait until after the release.

[andreasabel]

@UlfNorell : Do you intend to fix this for 2.7.0?

[andreasabel]

Does this mean that the following documentation is incorrect now?

agda/doc/user-manual/tools/auto.rst

Lines 104 to 113 in bdcbe48

	Dependencies between meta variables
	-----------------------------------
	If the goal type or type of local variables contain meta variables,
	then the constraints for these are also included in the search. If a
	solution is found it means that Auto has also found solutions for the
	occurring meta variables. Those solutions will be inserted into your
	file along with that of the hole from where you called Auto. Also, any
	unsolved equality constraints that contain any of the involved meta
	variables are respected in the search.

We'll need an intermediate fix for the docs then.

[andreasabel]

I added a disclaminer in #7372.