Commit 40ca6265 authored by Robbert Krebbers's avatar Robbert Krebbers

Rename fallthrough (instances) into default.

parent c02c0693
......@@ -140,7 +140,7 @@ Hint Mode SetUnfold + - : typeclass_instances.
Class SetUnfoldSimpl (P Q : Prop) := { set_unfold_simpl : SetUnfold P Q }.
Hint Extern 0 (SetUnfoldSimpl _ _) => csimpl; constructor : typeclass_instances.
Instance set_unfold_fallthrough P : SetUnfold P P | 1000. done. Qed.
Instance set_unfold_default P : SetUnfold P P | 1000. done. Qed.
Definition set_unfold_1 `{SetUnfold P Q} : P Q := proj1 (set_unfold P Q).
Definition set_unfold_2 `{SetUnfold P Q} : Q P := proj2 (set_unfold P Q).
......
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