diff --git a/theories/fin_maps.v b/theories/fin_maps.v index daef62bb6e29dda72ff57f0deb55ddd96d7e8900..1581f20db6bed50e61177e189eff236480701a88 100644 --- a/theories/fin_maps.v +++ b/theories/fin_maps.v @@ -3,7 +3,7 @@ (** Finite maps associate data to keys. This file defines an interface for finite maps and collects some theory on it. Most importantly, it proves useful induction principles for finite maps and implements the tactic -[simplify_map_equality] to simplify goals involving finite maps. *) +[simplify_map_eq] to simplify goals involving finite maps. *) From Coq Require Import Permutation. From stdpp Require Export relations vector orders.