Verified Commit a806150e authored by Paolo G. Giarrusso's avatar Paolo G. Giarrusso
Browse files

Mode for Equiv

parent a78b08fa
......@@ -7,3 +7,7 @@ Ltac done := stdpp.tactics.done.
(** Iris itself and many dependencies still rely on this coercion. *)
Coercion Z.of_nat : nat >-> Z.
(* No Hint Mode set in stdpp because of Coq bugs #5735 and #9058, only
fixed in Coq >= 8.12, which Iris depends on. *)
Global Hint Mode Equiv ! : typeclass_instances.
Markdown is supported
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