...
 
Commits (1)
......@@ -39,6 +39,13 @@ Obligation Tactic := idtac.
(** 3. Hide obligations from the results of the [Search] commands. *)
Add Search Blacklist "_obligation_".
(** Restrict Mode of some stdlib typeclasses. *)
Hint Mode Reflexive ! ! : typeclass_instances.
(* This needs a new instance to not break rewriting, see
https://github.com/coq/coq/issues/7916. *)
Instance: forall T (f : T -> Prop), Proper (eq ==> iff) f.
Proof. now intros T f x y ->. Qed.
(** * Sealing off definitions *)
Section seal.
Local Set Primitive Projections.
......