From f77e0ade09d8fd17add98c3bc4317627078f3aa8 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Fri, 30 May 2008 12:26:57 +0000
Subject: [PATCH] Suppression de 'exten', inutilise
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@646 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
lib/Maps.v | 6 ------
1 file changed, 6 deletions(-)
diff --git a/lib/Maps.v b/lib/Maps.v
index 4a346c6cf..4209fe6ec 100644
--- a/lib/Maps.v
+++ b/lib/Maps.v
@@ -1125,12 +1125,6 @@ Module EMap(X: EQUALITY_TYPE) <: MAP.
Proof.
intros. unfold get, map. reflexivity.
Qed.
- Lemma exten:
- forall (A: Set) (m1 m2: t A),
- (forall x: X.t, m1 x = m2 x) -> m1 = m2.
- Proof.
- intros. unfold t. apply extensionality. assumption.
- Qed.
End EMap.
(** * Useful notations *)
--
GitLab