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 ?
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
Last updated: Jan 29 2023 at 19:02 UTC