From 3e630f05c7ea04336006c50d11a212c8622bb22a Mon Sep 17 00:00:00 2001 From: Ralf Jung <jung@mpi-sws.org> Date: Mon, 9 May 2022 10:27:26 +0200 Subject: [PATCH] dom: make D type agument name consistent --- theories/base.v | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/theories/base.v b/theories/base.v index 59118414..010b34e6 100644 --- a/theories/base.v +++ b/theories/base.v @@ -1304,10 +1304,10 @@ Global Instance: Params (@partial_alter) 4 := {}. Global Arguments partial_alter _ _ _ _ _ !_ !_ / : simpl nomatch, assert. (** The function [dom m] should yield the domain of [m]. That is a finite -set of type [C] that contains the keys that are a member of [m]. -[C] is an output of the typeclass, i.e., there can be only one instance per map +set of type [D] that contains the keys that are a member of [m]. +[D] is an output of the typeclass, i.e., there can be only one instance per map type [M]. *) -Class Dom (M C : Type) := dom: M → C. +Class Dom (M D : Type) := dom: M → D. Global Hint Mode Dom ! - : typeclass_instances. Global Instance: Params (@dom) 3 := {}. Global Arguments dom : clear implicits. -- GitLab