coqSearching for an existing fact with Search and variants


Syntax

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

Parameters

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

Remarks

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.