Commit c215b6cc authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Hide `_unseal` in results of `Search`.

parent 85d5291f
......@@ -46,8 +46,10 @@ introduces all variables and gives them fresh names. As such, it becomes
impossible to refer to hypotheses in a robust way. *)
Obligation Tactic := idtac.
(** 3. Hide obligations from the results of the [Search] commands. *)
(** 3. Hide obligations and unsealing lemmas from the results of the [Search]
commands. *)
Add Search Blacklist "_obligation_".
Add Search Blacklist "_unseal".
(** * Sealing off definitions *)
Section seal.
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment