From f77e0ade09d8fd17add98c3bc4317627078f3aa8 Mon Sep 17 00:00:00 2001 From: xleroy Date: Fri, 30 May 2008 12:26:57 +0000 Subject: 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(-) (limited to 'lib/Maps.v') 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 *) -- cgit