From 05c5d5fd8fc0cf19a172f499d915ba0ca9bfc15b Mon Sep 17 00:00:00 2001 From: Ralf Jung <jung@mpi-sws.org> Date: Sun, 21 Feb 2016 13:55:38 +0100 Subject: [PATCH] move the proofs that we can perform stps in the STS to their own lemmas --- theories/fin_maps.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/fin_maps.v b/theories/fin_maps.v index daef62bb..1581f20d 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. -- GitLab