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

1 files changed, 2 insertions, 2 deletions

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':