Derive keys.

stdpp/base.v

@@ -1201,7 +1201,7 @@ Notation "'guard' P 'as' H ; z" := (mguard P (λ H, z))
 on maps. In the file [fin_maps] we will axiomatize finite maps.
 The function look up [m !! k] should yield the element at key [k] in [m]. *)
 Class Lookup (K A M : Type) := lookup: K → M → option A.
-Global Hint Mode Lookup + + ! : typeclass_instances.
+Global Hint Mode Lookup - + ! : typeclass_instances.
 Global Hint Mode Lookup - - + : typeclass_instances.
 Global Instance: Params (@lookup) 4 := {}.
 Notation "m !! i" := (lookup i m) (at level 20) : stdpp_scope.
@@ -1213,7 +1213,7 @@ Global Arguments lookup _ _ _ _ !_ !_ / : simpl nomatch, assert.
 (** The function [lookup_total] should be the total over-approximation
 of the partial [lookup] function. *)
 Class LookupTotal (K A M : Type) := lookup_total : K → M → A.
-Global Hint Mode LookupTotal + + ! : typeclass_instances.
+Global Hint Mode LookupTotal - + ! : typeclass_instances.
 Global Hint Mode LookupTotal - - + : typeclass_instances.
 Global Instance: Params (@lookup_total) 4 := {}.
 Notation "m !!! i" := (lookup_total i m) (at level 20) : stdpp_scope.
@@ -1224,7 +1224,7 @@ Global Arguments lookup_total _ _ _ _ !_ !_ / : simpl nomatch, assert.
 
 (** The singleton map *)
 Class SingletonM K A M := singletonM: K → A → M.
-Global Hint Mode SingletonM + + ! : typeclass_instances.
+Global Hint Mode SingletonM - + ! : typeclass_instances.
 Global Hint Mode SingletonM - - + : typeclass_instances.
 Global Instance: Params (@singletonM) 5 := {}.
 Notation "{[ k := a ]}" := (singletonM k a) (at level 1) : stdpp_scope.
@@ -1232,7 +1232,7 @@ Notation "{[ k := a ]}" := (singletonM k a) (at level 1) : stdpp_scope.
 (** The function insert [<[k:=a]>m] should update the element at key [k] with
 value [a] in [m]. *)
 Class Insert (K A M : Type) := insert: K → A → M → M.
-Global Hint Mode Insert + + ! : typeclass_instances.
+Global Hint Mode Insert - + ! : typeclass_instances.
 Global Hint Mode Insert - - + : typeclass_instances.
 Global Instance: Params (@insert) 5 := {}.
 Notation "<[ k := a ]>" := (insert k a)
@@ -1312,7 +1312,6 @@ Notation "{[ k1 := a1 ; k2 := a2 ; k3 := a3 ; k4 := a4 ; k5 := a5 ; k6 := a6 ; k
 [m]. If the key [k] is not a member of [m], the original map should be
 returned. *)
 Class Delete (K M : Type) := delete: K → M → M.
-Global Hint Mode Delete + ! : typeclass_instances.
 Global Hint Mode Delete - + : typeclass_instances.
 Global Instance: Params (@delete) 4 := {}.
 Global Arguments delete _ _ _ !_ !_ / : simpl nomatch, assert.
@@ -1320,7 +1319,7 @@ Global Arguments delete _ _ _ !_ !_ / : simpl nomatch, assert.
 (** The function [alter f k m] should update the value at key [k] using the
 function [f], which is called with the original value. *)
 Class Alter (K A M : Type) := alter: (A → A) → K → M → M.
-Global Hint Mode Alter + + ! : typeclass_instances.
+Global Hint Mode Alter - + ! : typeclass_instances.
 Global Hint Mode Alter - - + : typeclass_instances.
 Global Instance: Params (@alter) 4 := {}.
 Global Arguments alter {_ _ _ _} _ !_ !_ / : simpl nomatch, assert.
@@ -1331,7 +1330,7 @@ if [k] is not a member of [m]. The value at [k] should be deleted if [f]
 yields [None]. *)
 Class PartialAlter (K A M : Type) :=
   partial_alter: (option A → option A) → K → M → M.
-Global Hint Mode PartialAlter + + ! : typeclass_instances.
+Global Hint Mode PartialAlter - + ! : typeclass_instances.
 Global Hint Mode PartialAlter - - + : typeclass_instances.
 Global Instance: Params (@partial_alter) 4 := {}.
 Global Arguments partial_alter _ _ _ _ _ !_ !_ / : simpl nomatch, assert.