diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2008-05-30 12:26:57 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2008-05-30 12:26:57 +0000 |
commit | f77e0ade09d8fd17add98c3bc4317627078f3aa8 (patch) | |
tree | ad0991062e1da83d47a1e31eaf52ca96fb42d788 | |
parent | 1233298563ffb1d2b72a7caecd0c6c4e275100eb (diff) | |
download | compcert-f77e0ade09d8fd17add98c3bc4317627078f3aa8.tar.gz compcert-f77e0ade09d8fd17add98c3bc4317627078f3aa8.zip |
Suppression de 'exten', inutilise
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@646 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
-rw-r--r-- | lib/Maps.v | 6 |
1 files changed, 0 insertions, 6 deletions
@@ -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 *) |