1 files changed, 3 insertions, 4 deletions
diff --git a/theories/FSets/FMapList.v b/theories/FSets/FMapList.v
index f15ab222c..64d5b1c9a 100644
--- a/theories/FSets/FMapList.v
+++ b/theories/FSets/FMapList.v
@@ -527,7 +527,7 @@ Fixpoint mapi (f: key -> elt -> elt') (m:t elt) : t elt' :=
    | nil => nil
    | (k,e)::m' => (k,f k e) :: mapi f m'
   end.
-
+ 
 End Elt.
 Section Elt2.
 (* A new section is necessary for previous definitions to work
@@ -543,14 +543,13 @@ Proof.
  intros m x e f.
  (* functional induction map elt elt' f m.  *) (* Marche pas ??? *)
  induction m.
- inversion 1.
+ inversion 1. 
 
  destruct a as (x',e').
  simpl.
- inversion_clear 1.
+ inversion_clear 1.  
  constructor 1.
  unfold eqke in *; simpl in *; intuition congruence.
- constructor 2.
  unfold MapsTo in *; auto.
 Qed.