coq Searching for an existing fact with Search and variants

Help us to keep this website almost Ad Free! It takes only 10 seconds of your time:
> Step 1: Go view our video on YouTube: EF Core Bulk Extensions
> Step 2: And Like the video. BONUS: You can also share it!


  • Search qualid. (* for Coq 8.4 and newer versions *)
  • SearchAbout qualid. (* deprecated synonym. *)


qualidThe identifier or pattern to search for. It can involve notations


Before Coq 8.4, Search had the meaning of the current SearchHead: only search for facts where the pattern matches in the conclusion of the statement.

Got any coq Question?