From 40ca6265b0b107787c513103b9bc84128b83cbc7 Mon Sep 17 00:00:00 2001 From: Robbert Krebbers <mail@robbertkrebbers.nl> Date: Tue, 5 Jul 2016 18:15:16 +0200 Subject: [PATCH] Rename fallthrough (instances) into default. --- theories/collections.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/collections.v b/theories/collections.v index 16a265da..1f404919 100644 --- a/theories/collections.v +++ b/theories/collections.v @@ -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). -- GitLab