From 8bc231b13803a3d9d5e1f90a7f8d768b202a66b3 Mon Sep 17 00:00:00 2001 From: xleroy Date: Tue, 12 Mar 2013 13:20:01 +0000 Subject: Bind some local defs with Let, makes extracted code cleaner git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2148 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- lib/Maps.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'lib') diff --git a/lib/Maps.v b/lib/Maps.v index 9aa59d0..f667ea4 100644 --- a/lib/Maps.v +++ b/lib/Maps.v @@ -1337,9 +1337,9 @@ Hypothesis H_rec: forall m a k v, T.get k m = None -> T.get k m_final = Some v -> P m a -> P (T.set k v m) (f a k v). -Definition f' (a: A) (p : T.elt * V) := f a (fst p) (snd p). +Let f' (a: A) (p : T.elt * V) := f a (fst p) (snd p). -Definition P' (l: list (T.elt * V)) (a: A) : Prop := +Let P' (l: list (T.elt * V)) (a: A) : Prop := forall m, list_equiv l (T.elements m) -> P m a. Remark H_base': -- cgit v1.2.3