Stream: math-comp users

Topic: ✔ Documentation of math-comp Search


view this post on Zulip Pierre Rousselin (Aug 13 2022 at 08:40):

I didn't find the description of the math-comp Search command in the reference manual. Is there a place where it is completely described with emphasis on the differences with the vanilla coq Search command ?

Is it possible to choose between the two commands ?

view this post on Zulip Pierre Roux (Aug 13 2022 at 09:00):

There is no more Search command specific to math-comp. Everybody now uses the regular Search command described in the refman https://coq.inria.fr/distrib/current/refman/proof-engine/vernacular-commands.html#coq:cmd.Search

view this post on Zulip Pierre Rousselin (Aug 13 2022 at 09:03):

Thank you, it is good to know.

view this post on Zulip Notification Bot (Aug 13 2022 at 09:04):

Pierre Rousselin has marked this topic as resolved.


Last updated: Jul 15 2024 at 21:02 UTC