search

ilyasergey / pnp

Lecture notes for a short course on proving/programming in Coq via SSReflect.
https://ilyasergey.net/pnp
BSD 2-Clause "Simplified" License
154 stars 17 forks source link

ssr-search-moved warning #25

Open anton-trunov opened 3 years ago

anton-trunov commented 3 years ago

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 commented 3 years ago

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).