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

Blacklist `_obligation_` for Search.

parent 8fc099dc
Pipeline #4012 passed with stage
in 6 minutes and 46 seconds
...@@ -12,7 +12,11 @@ From Coq Require Export Morphisms RelationClasses List Bool Utf8 Setoid. ...@@ -12,7 +12,11 @@ From Coq Require Export Morphisms RelationClasses List Bool Utf8 Setoid.
Set Default Proof Using "Type". Set Default Proof Using "Type".
Export ListNotations. Export ListNotations.
From Coq.Program Require Export Basics Syntax. From Coq.Program Require Export Basics Syntax.
(* Tweak program: don't let it automatically simplify obligations and hide
them from the results of the [Search] commands. *)
Obligation Tactic := idtac. Obligation Tactic := idtac.
Add Search Blacklist "_obligation_".
(** Sealing off definitions *) (** Sealing off definitions *)
Set Primitive Projections. Set Primitive Projections.
......
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