ssr-search-moved warning

[anton-trunov]

trafficstars

There is a bunch of ssr-search-moved warnings:

File "./coq/HTT.v", line 1465, characters 0-18:
Warning: SSReflect's Search command has been moved to the ssrsearch module;
please Require that module if you still want to use SSReflect's Search
command [ssr-search-moved,deprecated]

I guess this is better fixed when there is a Coq release actually disabling the SSReflect style search utility.

[anton-trunov]

There is also a couple of new warnings connected to this one, e.g.

File "./coq/FunProg.v", line 919, characters 0-23:
Warning: Casts are ignored in patterns [cast-in-pattern,automation]

It's for these two lines:

Search _ (_ * _ : nat).

and

Search _ (_ * _: Type).