Suppression de 'exten', inutilise

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@646 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 0 insertions, 6 deletions

diff --git a/lib/Maps.v b/lib/Maps.v
index 4a346c6c..4209fe6e 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 *)