Merge branch 'v8.5' into trunk

22 files changed, 1113 insertions, 196 deletions

diff --git a/doc/refman/Cases.tex b/doc/refman/Cases.tex
index 51ec2ef818..4238bf6a57 100644
--- a/doc/refman/Cases.tex
+++ b/doc/refman/Cases.tex
@@ -194,7 +194,7 @@ system. Here is an example:
 Set Printing Depth 50.
 \end{coq_eval}
 \begin{coq_example}
-Check (fun x:nat =>
+Fail Check (fun x:nat =>
          match x with
          | O => true
          | S _ => false
@@ -271,7 +271,7 @@ When we use parameters in patterns there is an error message:
 Set Printing Depth 50.
 \end{coq_eval}
 \begin{coq_example}
-Check
+Fail Check
   (fun l:List nat =>
      match l with
      | nil A => nil nat
diff --git a/doc/refman/Classes.tex b/doc/refman/Classes.tex
index 069b991274..e8ebb9f995 100644
--- a/doc/refman/Classes.tex
+++ b/doc/refman/Classes.tex
@@ -107,7 +107,7 @@ satisfied by \texttt{{eqa : EqDec A}}. In case no satisfying constraint can be
 found, an error is raised:
 
 \begin{coq_example}
-Definition neqb' (A : Type) (x y : A) := negb (eqb x y).
+Fail Definition neqb' (A : Type) (x y : A) := negb (eqb x y).
 \end{coq_example}
 
 The algorithm used to solve constraints is a variant of the eauto tactic
diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex
index 1cce48b95b..3fd5ae0b24 100644
--- a/doc/refman/RefMan-cic.tex
+++ b/doc/refman/RefMan-cic.tex
@@ -742,11 +742,11 @@ there is an occurrence of \List\ which is not applied to the parameter
 variable in the conclusion of the type of {\tt cons'}:
 \begin{coq_eval}
 Set Printing Depth 50.
-(********** The following is not correct and should produce **********)
-(********* Error: The 1st argument of list' must be A in ... *********)
 \end{coq_eval}
+% (********** The following is not correct and should produce **********)
+% (********* Error: The 1st argument of list' must be A in ... *********)
 \begin{coq_example}
-Inductive list' (A:Set) : Set :=
+Fail Inductive list' (A:Set) : Set :=
   | nil' : list' A
   | cons' : A -> list' A -> list' (A*A).
 \end{coq_example}
@@ -919,12 +919,10 @@ Inductive exProp (P:Prop->Prop) : Prop
   := exP_intro : forall X:Prop, P X -> exProp P.
 \end{coq_example*}
 The same definition on \Set{} is not allowed and fails:
-\begin{coq_eval}
-(********** The following is not correct and should produce **********)
-(*** Error: Large non-propositional inductive types must be in Type***)
-\end{coq_eval}
+% (********** The following is not correct and should produce **********)
+% (*** Error: Large non-propositional inductive types must be in Type***)
 \begin{coq_example}
-Inductive exSet (P:Set->Prop) : Set 
+Fail Inductive exSet (P:Set->Prop) : Set
   := exS_intro : forall X:Set, P X -> exSet P.
 \end{coq_example}
 It is possible to declare the same inductive definition in the
@@ -1282,14 +1280,11 @@ Inductive or (A B:Prop) : Prop :=
 \end{coq_example*}
 The following definition which computes a boolean value by case over
 the proof of \texttt{or A B} is not accepted:
-\begin{coq_eval}
-(***************************************************************)
-(*** This example should fail with ``Incorrect elimination'' ***)
-\end{coq_eval}
+% (***************************************************************)
+% (*** This example should fail with ``Incorrect elimination'' ***)
 \begin{coq_example}
-Set Asymmetric Patterns.
-Definition choice (A B: Prop) (x:or A B) := 
-   match x with or_introl a => true | or_intror b => false end.
+Fail Definition choice (A B: Prop) (x:or A B) :=
+  match x with or_introl _ _ a => true | or_intror _ _ b => false end.
 \end{coq_example}
 From the computational point of view, the structure of the proof of
 \texttt{(or A B)} in this term is needed for computing the boolean
@@ -1592,8 +1587,8 @@ Fixpoint plus (n m:nat) {struct n} : nat :=
 Print plus.
 Fixpoint lgth (A:Set) (l:list A) {struct l} : nat :=
   match l with
-  | nil => O
-  | cons a l' => S (lgth A l')
+  | nil _ => O
+  | cons _ a l' => S (lgth A l')
   end.
 Print lgth.
 Fixpoint sizet (t:tree) : nat := let (f) := t in S (sizef f)
@@ -1632,13 +1627,11 @@ Definition sont (t:tree) : forest
    := let (f) := t in f.
 \end{coq_example}
 The following is not a conversion but can be proved after a case analysis.
-\begin{coq_eval}
-(******************************************************************)
-(** Error: Impossible to unify ....                              **)
-\end{coq_eval}
+% (******************************************************************)
+% (** Error: Impossible to unify ....                              **)
 \begin{coq_example}
 Goal forall t:tree, sizet t = S (sizef (sont t)).
-reflexivity. (** this one fails **)
+Fail reflexivity.
 destruct t.
 reflexivity.
 \end{coq_example}
@@ -1701,16 +1694,13 @@ by using the compiler option \texttt{-impredicative-set}.
 
 For example, using the ordinary \texttt{coqtop} command, the following
 is rejected.
-\begin{coq_eval}
-(** This example should fail *******************************
-    Error: The term forall X:Set, X -> X has type Type
-    while it is expected to have type Set
-***)
-\end{coq_eval}
+% (** This example should fail *******************************
+%     Error: The term forall X:Set, X -> X has type Type
+%     while it is expected to have type Set ***)
 \begin{coq_example}
-Definition id: Set := forall X:Set,X->X.
+Fail Definition id: Set := forall X:Set,X->X.
 \end{coq_example}
-while it will type-check, if one use instead the \texttt{coqtop
+while it will type-check, if one uses instead the \texttt{coqtop
   -impredicative-set} command.
 
 The major change in the theory concerns the rule for product formation
diff --git a/doc/refman/RefMan-decl.tex b/doc/refman/RefMan-decl.tex
index c84e3a9dfa..aae10e323c 100644
--- a/doc/refman/RefMan-decl.tex
+++ b/doc/refman/RefMan-decl.tex
@@ -192,7 +192,7 @@ later.
 Theorem this_is_not_so_trivial: False.
 proof.
 end proof. (* here a warning is issued *)
-Qed. (* fails: the proof in incomplete *)
+Fail Qed. (* fails: the proof in incomplete *)
 Admitted. (* Oops! *)
 \end{coq_example}
 \begin{coq_eval}
@@ -404,7 +404,7 @@ proof.
 \end{coq_eval} 
 \begin{coq_example}
 Show.
-hence C. (* fails *)
+Fail hence C. (* fails *)
 \end{coq_example}
 \begin{coq_eval}
 Abort.
@@ -578,7 +578,7 @@ let P:(nat -> Prop).
 \end{coq_eval} 
 \begin{coq_example}
 Show.
-let x. (* fails because x's type is not clear *) 
+Fail let x. (* fails because x's type is not clear *)
 let x be such that HP:(P x). (* here x's type is inferred from (P x) *)
 \end{coq_example}
 \begin{coq_eval}
diff --git a/doc/refman/RefMan-gal.tex b/doc/refman/RefMan-gal.tex
index 0d628ac7ee..cf83d0c722 100644
--- a/doc/refman/RefMan-gal.tex
+++ b/doc/refman/RefMan-gal.tex
@@ -1155,7 +1155,7 @@ Inductive list2 (A:Set) : Set := nil2 | cons2 (_:A) (_:list2 (A*A)).
 \end{coq_example*}
 But the following definition will give an error:
 \begin{coq_example}
-Inductive listw (A:Set) : Set :=
+Fail Inductive listw (A:Set) : Set :=
   | nilw : listw (A*A)
   | consw : A -> listw (A*A) -> listw (A*A).
 \end{coq_example}
@@ -1401,11 +1401,11 @@ error message:
 
 \begin{coq_eval}
 Set Printing Depth 50.
-(********** The following is not correct and should produce **********)
-(*********      Error: Recursive call to wrongplus ...      **********)
 \end{coq_eval}
+% (********** The following is not correct and should produce **********)
+% (*********      Error: Recursive call to wrongplus ...      **********)
 \begin{coq_example}
-Fixpoint wrongplus (n m:nat) {struct n} : nat :=
+Fail Fixpoint wrongplus (n m:nat) {struct n} : nat :=
   match m with
   | O => n
   | S p => S (wrongplus n p)
@@ -1530,11 +1530,11 @@ function does not satisfy the guard condition:
 
 \begin{coq_eval}
 Set Printing Depth 50.
-(********** The following is not correct and should produce **********)
-(***************** Error: Unguarded recursive call *******************)
 \end{coq_eval}
+% (********** The following is not correct and should produce **********)
+% (***************** Error: Unguarded recursive call *******************)
 \begin{coq_example}
-CoFixpoint filter (p:nat -> bool) (s:Stream) : Stream :=
+Fail CoFixpoint filter (p:nat -> bool) (s:Stream) : Stream :=
   if p (hd s) then Seq (hd s) (filter p (tl s)) else filter p (tl s).
 \end{coq_example}
 
diff --git a/doc/refman/RefMan-mod.tex b/doc/refman/RefMan-mod.tex
index f48cf6abf5..48b9315e37 100644
--- a/doc/refman/RefMan-mod.tex
+++ b/doc/refman/RefMan-mod.tex
@@ -238,14 +238,14 @@ as the body of \texttt{x}.
 
 \begin{coq_eval}
 Set Printing Depth 50.
-(********** The following is not correct and should produce **********)
-(***************** Error: N.y not a defined object *******************)
 \end{coq_eval}
+% (********** The following is not correct and should produce **********)
+% (***************** Error: N.y not a defined object *******************)
 \begin{coq_example}
 Module N  :  SIG with Definition T := nat  :=  M.
 Print N.T.
 Print N.x.
-Print N.y.
+Fail Print N.y.
 \end{coq_example}
 \begin{coq_eval}
 Reset N.
@@ -353,15 +353,11 @@ Example:
 
 \begin{coq_example}
 Module Mod.
-\end{coq_example}
-\begin{coq_example}
   Definition T:=nat.
   Check T.
-\end{coq_example}
-\begin{coq_example}
 End Mod.
 Check Mod.T.
-Check T. (* Incorrect ! *)
+Fail Check T. (* Incorrect! *)
 Import Mod.
 Check T. (* Now correct *)
 \end{coq_example}
@@ -386,7 +382,7 @@ Local Definition T := nat.
 End B.
 End A.
 Import A.
-Check B.T.
+Fail Check B.T.
 \end{coq_example}
 
 \begin{Variants}
diff --git a/doc/refman/RefMan-syn.tex b/doc/refman/RefMan-syn.tex
index 15ddf62611..107b98f010 100644
--- a/doc/refman/RefMan-syn.tex
+++ b/doc/refman/RefMan-syn.tex
@@ -434,7 +434,7 @@ notation are replaced by ``\_''.
 \Example
 \begin{coq_example}
 Locate "exists".
-Locate "'exists' _ , _".
+Locate "exists _ .. _ , _".
 \end{coq_example}
 
 \SeeAlso Section \ref{Locate}.
@@ -516,11 +516,11 @@ the next command fails because {\tt p} does not bind in
 the instance of {\tt n}.
 \begin{coq_eval}
 Set Printing Depth 50.
-(********** The following produces **********)
-(**** The reference p was not found in the current environment ********)
 \end{coq_eval}
+% (********** The following produces **********)
+% (**** The reference p was not found in the current environment ********)
 \begin{coq_example}
-Check (exists_different p).
+Fail Check (exists_different p).
 \end{coq_example}
 
 \Rem Binding variables must not necessarily be parsed using the
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index c3d8ad5318..52f32d0c7d 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -343,7 +343,7 @@ Section~\ref{pattern} to transform the goal so that it gets the form
   This behaves like {\tt apply} but it reasons modulo conversion only
   on subterms that contain no variables to instantiate. For instance,
   the following example does not succeed because it would require the
-  conversion of {\tt id ?1234} and {\tt O}.
+  conversion of {\tt id ?foo} and {\tt O}.
 
 \begin{coq_eval}
 Reset Initial.
@@ -354,7 +354,7 @@ Hypothesis H : forall y, id y = y.
 Goal O = O.
 \end{coq_example*}
 \begin{coq_example}
-simple apply H.
+Fail simple apply H.
 \end{coq_example}
 
   Because it reasons modulo a limited amount of conversion, {\tt
@@ -419,7 +419,7 @@ no value for {\tt y} in {\tt Rtrans} is found by {\tt apply}:
 %(**** Error: generated subgoal (R n ?17) has metavariables in it *****)
 %\end{coq_eval}
 \begin{coq_example}
-apply Rtrans.
+Fail apply Rtrans.
 \end{coq_example}
 
 A solution is to apply {\tt (Rtrans n m p)} or {\tt (Rtrans n m)}.
@@ -914,10 +914,10 @@ containing {\tt *} or {\tt **}, {\tt intros $p_1$ ... $p_n$}
 \begin{coq_example}
 Goal forall A B C:Prop, A \/ B /\ C -> (A -> C) -> C.
 intros * [a | (_,c)] f.
-apply (f a).
-exact c.
-Qed.
 \end{coq_example}
+\begin{coq_eval}
+Abort.
+\end{coq_eval}
 
 \Rem {\tt intros $p_1~\ldots~p_n$} is not fully equivalent to
 \texttt{intros $p_1$;\ldots; intros $p_n$} for the following reasons:
@@ -935,7 +935,7 @@ Qed.
 Goal forall n:nat, n = 0 -> n = 0.
 intros [ | ] H.
 Show 2.
-Undo 2.
+Undo.
 intros [ | ]; intros H.
 Show 2.
 \end{coq_example}
diff --git a/test-suite/output/Arguments.out b/test-suite/output/Arguments.out
index 629a1ab632..9c488ce5af 100644
--- a/test-suite/output/Arguments.out
+++ b/test-suite/output/Arguments.out
@@ -110,8 +110,8 @@ Expands to: Constant Top.f
 forall w : r, w 3 true = tt
      : Prop
 The command has indeed failed with message:
-=> Error: Unknown interpretation for notation "$".
+Error: Unknown interpretation for notation "$".
 w 3 true = tt
      : Prop
 The command has indeed failed with message:
-=> Error: Extra argument _.
+Error: Extra argument _.
diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out
index c29f564945..9331f29fb5 100644
--- a/test-suite/output/Arguments_renaming.out
+++ b/test-suite/output/Arguments_renaming.out
@@ -1,8 +1,8 @@
 The command has indeed failed with message:
-=> Error: To rename arguments the "rename" flag must be specified.
+Error: To rename arguments the "rename" flag must be specified.
 Argument A renamed to B.
 The command has indeed failed with message:
-=> Error: To rename arguments the "rename" flag must be specified.
+Error: To rename arguments the "rename" flag must be specified.
 Argument A renamed to T.
 @eq_refl
      : forall (B : Type) (y : B), y = y
@@ -106,15 +106,15 @@ Expands to: Constant Top.myplus
 @myplus
      : forall Z : Type, Z -> nat -> nat -> nat
 The command has indeed failed with message:
-=> Error: All arguments lists must declare the same names.
+Error: All arguments lists must declare the same names.
 The command has indeed failed with message:
-=> Error: The following arguments are not declared: x.
+Error: The following arguments are not declared: x.
 The command has indeed failed with message:
-=> Error: Arguments names must be distinct.
+Error: Arguments names must be distinct.
 The command has indeed failed with message:
-=> Error: Argument z cannot be declared implicit.
+Error: Argument z cannot be declared implicit.
 The command has indeed failed with message:
-=> Error: Extra argument y.
+Error: Extra argument y.
 The command has indeed failed with message:
-=> Error: To rename arguments the "rename" flag must be specified.
+Error: To rename arguments the "rename" flag must be specified.
 Argument A renamed to R.
diff --git a/test-suite/output/Errors.out b/test-suite/output/Errors.out
index bcc37b635d..6354ad469e 100644
--- a/test-suite/output/Errors.out
+++ b/test-suite/output/Errors.out
@@ -1,7 +1,7 @@
 The command has indeed failed with message:
-=> Error: The field t is missing in Top.M.
+The field t is missing in Top.M.
 The command has indeed failed with message:
-=> Error: Unable to unify "nat" with "True".
+Unable to unify "nat" with "True".
 The command has indeed failed with message:
-=> In nested Ltac calls to "f" and "apply x", last call failed.
-Error: Unable to unify "nat" with "True".
+In nested Ltac calls to "f" and "apply x", last call failed.
+Unable to unify "nat" with "True".
diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out
index 60ee72b363..6efd671a8c 100644
--- a/test-suite/output/Notations.out
+++ b/test-suite/output/Notations.out
@@ -41,29 +41,29 @@ fun x : nat => ifn x is succ n then n else 0
 -4
      : Z
 The command has indeed failed with message:
-=> Error: x should not be bound in a recursive pattern of the right-hand side.
+Error: x should not be bound in a recursive pattern of the right-hand side.
 The command has indeed failed with message:
-=> Error: in the right-hand side, y and z should appear in
+Error: in the right-hand side, y and z should appear in
 term position as part of a recursive pattern.
 The command has indeed failed with message:
-=> Error: The reference w was not found in the current environment.
+The reference w was not found in the current environment.
 The command has indeed failed with message:
-=> Error: in the right-hand side, y and z should appear in
+Error: in the right-hand side, y and z should appear in
 term position as part of a recursive pattern.
 The command has indeed failed with message:
-=> Error: z is expected to occur in binding position in the right-hand side.
+Error: z is expected to occur in binding position in the right-hand side.
 The command has indeed failed with message:
-=> Error: as y is a non-closed binder, no such "," is allowed to occur.
+Error: as y is a non-closed binder, no such "," is allowed to occur.
 The command has indeed failed with message:
-=> Error: Cannot find where the recursive pattern starts.
+Error: Cannot find where the recursive pattern starts.
 The command has indeed failed with message:
-=> Error: Cannot find where the recursive pattern starts.
+Error: Cannot find where the recursive pattern starts.
 The command has indeed failed with message:
-=> Error: Cannot find where the recursive pattern starts.
+Error: Cannot find where the recursive pattern starts.
 The command has indeed failed with message:
-=> Error: Cannot find where the recursive pattern starts.
+Error: Cannot find where the recursive pattern starts.
 The command has indeed failed with message:
-=> Error: Both ends of the recursive pattern are the same.
+Error: Both ends of the recursive pattern are the same.
 SUM (nat * nat) nat
      : Set
 FST (0; 1)
diff --git a/test-suite/output/names.out b/test-suite/output/names.out
index 2892dfd5a1..9471b892dd 100644
--- a/test-suite/output/names.out
+++ b/test-suite/output/names.out
@@ -1,5 +1,4 @@
 The command has indeed failed with message:
-=> Error:
 In environment
 y : nat
 The term "a y" has type "{y0 : nat | y = y0}"
diff --git a/test-suite/output/rewrite-2172.out b/test-suite/output/rewrite-2172.out
index 30385072c2..27b0dc1b7b 100644
--- a/test-suite/output/rewrite-2172.out
+++ b/test-suite/output/rewrite-2172.out
@@ -1,2 +1,2 @@
 The command has indeed failed with message:
-=> Error: Unable to find an instance for the variable E.
+Unable to find an instance for the variable E.
diff --git a/theories/MMaps/MMapPositive.v b/theories/MMaps/MMapPositive.v
new file mode 100644
index 0000000000..2da1fff1e5
--- /dev/null
+++ b/theories/MMaps/MMapPositive.v
@@ -0,0 +1,937 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(** * MMapPositive : an implementation of MMapInterface for [positive] keys. *)
+
+Require Import Bool BinPos Orders OrdersEx OrdersLists MMapInterface.
+
+Set Implicit Arguments.
+Local Open Scope lazy_bool_scope.
+Local Open Scope positive_scope.
+Local Unset Elimination Schemes.
+
+(** This file is an adaptation to the [MMap] framework of a work by
+  Xavier Leroy and Sandrine Blazy (used for building certified compilers).
+  Keys are of type [positive], and maps are binary trees: the sequence
+  of binary digits of a positive number corresponds to a path in such a tree.
+  This is quite similar to the [IntMap] library, except that no path
+  compression is implemented, and that the current file is simple enough to be
+  self-contained. *)
+
+(** First, some stuff about [positive] *)
+
+Fixpoint append (i j : positive) : positive :=
+    match i with
+      | xH => j
+      | xI ii => xI (append ii j)
+      | xO ii => xO (append ii j)
+    end.
+
+Lemma append_assoc_0 :
+  forall (i j : positive), append i (xO j) = append (append i (xO xH)) j.
+Proof.
+ induction i; intros; destruct j; simpl;
+ try rewrite (IHi (xI j));
+ try rewrite (IHi (xO j));
+ try rewrite <- (IHi xH);
+ auto.
+Qed.
+
+Lemma append_assoc_1 :
+  forall (i j : positive), append i (xI j) = append (append i (xI xH)) j.
+Proof.
+ induction i; intros; destruct j; simpl;
+ try rewrite (IHi (xI j));
+ try rewrite (IHi (xO j));
+ try rewrite <- (IHi xH);
+ auto.
+Qed.
+
+Lemma append_neutral_r : forall (i : positive), append i xH = i.
+Proof.
+ induction i; simpl; congruence.
+Qed.
+
+Lemma append_neutral_l : forall (i : positive), append xH i = i.
+Proof.
+ simpl; auto.
+Qed.
+
+(** The module of maps over positive keys *)
+
+Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
+
+  Module E:=PositiveOrderedTypeBits.
+  Module ME:=KeyOrderedType E.
+
+  Definition key := positive : Type.
+
+  Inductive tree (A : Type) :=
+    | Leaf : tree A
+    | Node : tree A -> option A -> tree A -> tree A.
+
+  Arguments Leaf {A}.
+
+  Scheme tree_ind := Induction for tree Sort Prop.
+
+  Definition t := tree.
+
+  Definition empty {A} : t A := Leaf.
+
+  Section A.
+  Variable A:Type.
+
+  Fixpoint is_empty (m : t A) : bool :=
+   match m with
+    | Leaf => true
+    | Node l None r => (is_empty l) &&& (is_empty r)
+    | _ => false
+   end.
+
+  Fixpoint find (i : key) (m : t A) : option A :=
+    match m with
+    | Leaf => None
+    | Node l o r =>
+        match i with
+        | xH => o
+        | xO ii => find ii l
+        | xI ii => find ii r
+        end
+    end.
+
+  Fixpoint mem (i : key) (m : t A) : bool :=
+    match m with
+    | Leaf => false
+    | Node l o r =>
+        match i with
+        | xH => match o with None => false | _ => true end
+        | xO ii => mem ii l
+        | xI ii => mem ii r
+        end
+    end.
+
+  Fixpoint add (i : key) (v : A) (m : t A) : t A :=
+    match m with
+    | Leaf =>
+        match i with
+        | xH => Node Leaf (Some v) Leaf
+        | xO ii => Node (add ii v Leaf) None Leaf
+        | xI ii => Node Leaf None (add ii v Leaf)
+        end
+    | Node l o r =>
+        match i with
+        | xH => Node l (Some v) r
+        | xO ii => Node (add ii v l) o r
+        | xI ii => Node l o (add ii v r)
+        end
+    end.
+
+  (** helper function to avoid creating empty trees that are not leaves *)
+
+  Definition node (l : t A) (o: option A) (r : t A) : t A :=
+    match o,l,r with
+      | None,Leaf,Leaf => Leaf
+      | _,_,_ => Node l o r
+    end.
+
+  Fixpoint remove (i : key) (m : t A) : t A :=
+    match m with
+    | Leaf => Leaf
+    | Node l o r =>
+      match i with
+      | xH => node l None r
+      | xO ii => node (remove ii l) o r
+      | xI ii => node l o (remove ii r)
+      end
+    end.
+
+  (** [bindings] *)
+
+  Fixpoint xbindings (m : t A) (i : key) : list (key * A) :=
+    match m with
+      | Leaf => nil
+      | Node l None r =>
+          (xbindings l (append i (xO xH))) ++ (xbindings r (append i (xI xH)))
+      | Node l (Some x) r =>
+          (xbindings l (append i (xO xH)))
+          ++ ((i, x) :: xbindings r (append i (xI xH)))
+    end.
+
+  (* Note: function [xbindings] above is inefficient.  We should apply
+     deforestation to it, but that makes the proofs even harder. *)
+
+  Definition bindings (m : t A) := xbindings m xH.
+
+  (** [cardinal] *)
+
+  Fixpoint cardinal (m : t A) : nat :=
+    match m with
+      | Leaf => 0%nat
+      | Node l None r => (cardinal l + cardinal r)%nat
+      | Node l (Some _) r => S (cardinal l + cardinal r)
+    end.
+
+  (** Specification proofs *)
+
+  Lemma gleaf : forall (i : key), find i Leaf = None.
+  Proof. destruct i; simpl; auto. Qed.
+
+  Theorem empty_spec:
+    forall (i: key), find i empty = None.
+  Proof. exact gleaf. Qed.
+
+  Theorem add_spec1:
+    forall (m: t A) (i: key) (x: A), find i (add i x m) = Some x.
+  Proof.
+    intros m i; revert m.
+    induction i; destruct m; simpl; auto.
+  Qed.
+
+  Theorem add_spec2:
+    forall (m: t A) (i j: key) (x: A),
+    i <> j -> find j (add i x m) = find j m.
+  Proof.
+    intros m i j; revert m i.
+    induction j; destruct i, m; simpl; intros;
+     rewrite ?IHj, ?gleaf; auto; try congruence.
+  Qed.
+
+  Lemma rleaf : forall (i : key), remove i Leaf = Leaf.
+  Proof. destruct i; simpl; auto. Qed.
+
+  Lemma gnode l o r i : find i (node l o r) = find i (Node l o r).
+  Proof.
+   destruct o,l,r; simpl; trivial.
+   destruct i; simpl; now rewrite ?gleaf.
+  Qed.
+
+  Opaque node.
+
+  Theorem remove_spec1:
+    forall (m: t A)(i: key), find i (remove i m) = None.
+  Proof.
+    induction m; simpl.
+    - intros; rewrite rleaf. apply gleaf.
+    - destruct i; simpl remove; rewrite gnode; simpl; auto.
+  Qed.
+
+  Theorem remove_spec2:
+    forall (m: t A)(i j: key),
+    i <> j -> find j (remove i m) = find j m.
+  Proof.
+    induction m; simpl; intros.
+    - now rewrite rleaf.
+    - destruct i; simpl; rewrite gnode; destruct j; simpl; trivial;
+      try apply IHm1; try apply IHm2; congruence.
+  Qed.
+
+  Lemma xbindings_correct:
+      forall (m: t A) (i j : key) (v: A),
+      find i m = Some v -> List.In (append j i, v) (xbindings m j).
+  Proof.
+    induction m; intros.
+    - rewrite (gleaf i) in H; discriminate.
+    - destruct o, i; simpl in *; apply in_or_app.
+      + rewrite append_assoc_1. right; now apply in_cons, IHm2.
+      + rewrite append_assoc_0. left; now apply IHm1.
+      + rewrite append_neutral_r. injection H as ->.
+        right; apply in_eq.
+      + rewrite append_assoc_1. right; now apply IHm2.
+      + rewrite append_assoc_0. left; now apply IHm1.
+      + discriminate.
+  Qed.
+
+  Theorem bindings_correct:
+    forall (m: t A) (i: key) (v: A),
+    find i m = Some v -> List.In (i, v) (bindings m).
+  Proof.
+    intros m i v H.
+    exact (xbindings_correct m i xH H).
+  Qed.
+
+  Fixpoint xfind (i j : key) (m : t A) : option A :=
+      match i, j with
+      | _, xH => find i m
+      | xO ii, xO jj => xfind ii jj m
+      | xI ii, xI jj => xfind ii jj m
+      | _, _ => None
+      end.
+
+  Lemma xfind_left :
+      forall (j i : key) (m1 m2 : t A) (o : option A) (v : A),
+      xfind i (append j (xO xH)) m1 = Some v ->
+      xfind i j (Node m1 o m2) = Some v.
+  Proof.
+    induction j; intros; destruct i; simpl; simpl in H; auto; try congruence.
+    destruct i; simpl in *; auto.
+  Qed.
+
+  Lemma xbindings_ii :
+    forall (m: t A) (i j : key) (v: A),
+      List.In (xI i, v) (xbindings m (xI j)) ->
+      List.In (i, v) (xbindings m j).
+  Proof.
+    induction m.
+    - simpl; auto.
+    - intros; destruct o; simpl in *; rewrite in_app_iff in *;
+      destruct H.
+      + left; now apply IHm1.
+      + right; destruct (in_inv H).
+        * injection H0 as -> ->. apply in_eq.
+        * apply in_cons; now apply IHm2.
+      + left; now apply IHm1.
+      + right; now apply IHm2.
+  Qed.
+
+  Lemma xbindings_io :
+    forall (m: t A) (i j : key) (v: A),
+      ~List.In (xI i, v) (xbindings m (xO j)).
+  Proof.
+    induction m.
+    - simpl; auto.
+    - intros; destruct o; simpl; intro H; destruct (in_app_or _ _ _ H).
+      + apply (IHm1 _ _ _ H0).
+      + destruct (in_inv H0). congruence. apply (IHm2 _ _ _ H1).
+      + apply (IHm1 _ _ _ H0).
+      + apply (IHm2 _ _ _ H0).
+  Qed.
+
+  Lemma xbindings_oo :
+      forall (m: t A) (i j : key) (v: A),
+      List.In (xO i, v) (xbindings m (xO j)) ->
+      List.In (i, v) (xbindings m j).
+  Proof.
+    induction m.
+    - simpl; auto.
+    - intros; destruct o; simpl; simpl in H; destruct (in_app_or _ _ _ H);
+      apply in_or_app.
+      + left; now apply IHm1.
+      + right; destruct (in_inv H0).
+        injection H1 as -> ->; apply in_eq.
+        apply in_cons; now apply IHm2.
+      + left; now apply IHm1.
+      + right; now apply IHm2.
+  Qed.
+
+  Lemma xbindings_oi :
+    forall (m: t A) (i j : key) (v: A),
+      ~List.In (xO i, v) (xbindings m (xI j)).
+  Proof.
+    induction m.
+    - simpl; auto.
+    - intros; destruct o; simpl; intro H; destruct (in_app_or _ _ _ H).
+      + apply (IHm1 _ _ _ H0).
+      + destruct (in_inv H0). congruence. apply (IHm2 _ _ _ H1).
+      + apply (IHm1 _ _ _ H0).
+      + apply (IHm2 _ _ _ H0).
+  Qed.
+
+  Lemma xbindings_ih :
+      forall (m1 m2: t A) (o: option A) (i : key) (v: A),
+      List.In (xI i, v) (xbindings (Node m1 o m2) xH) ->
+      List.In (i, v) (xbindings m2 xH).
+  Proof.
+    destruct o; simpl; intros; destruct (in_app_or _ _ _ H).
+    absurd (List.In (xI i, v) (xbindings m1 2)); auto; apply xbindings_io; auto.
+    destruct (in_inv H0).
+    congruence.
+    apply xbindings_ii; auto.
+    absurd (List.In (xI i, v) (xbindings m1 2)); auto; apply xbindings_io; auto.
+    apply xbindings_ii; auto.
+  Qed.
+
+  Lemma xbindings_oh :
+    forall (m1 m2: t A) (o: option A) (i : key) (v: A),
+      List.In (xO i, v) (xbindings (Node m1 o m2) xH) ->
+      List.In (i, v) (xbindings m1 xH).
+  Proof.
+    destruct o; simpl; intros; destruct (in_app_or _ _ _ H).
+    apply xbindings_oo; auto.
+    destruct (in_inv H0).
+    congruence.
+    absurd (List.In (xO i, v) (xbindings m2 3)); auto; apply xbindings_oi; auto.
+    apply xbindings_oo; auto.
+    absurd (List.In (xO i, v) (xbindings m2 3)); auto; apply xbindings_oi; auto.
+  Qed.
+
+  Lemma xbindings_hi :
+      forall (m: t A) (i : key) (v: A),
+      ~List.In (xH, v) (xbindings m (xI i)).
+  Proof.
+    induction m; intros.
+    - simpl; auto.
+    - destruct o; simpl; intro H; destruct (in_app_or _ _ _ H).
+      + generalize H0; apply IHm1; auto.
+      + destruct (in_inv H0). congruence.
+        generalize H1; apply IHm2; auto.
+      + generalize H0; apply IHm1; auto.
+      + generalize H0; apply IHm2; auto.
+  Qed.
+
+  Lemma xbindings_ho :
+    forall (m: t A) (i : key) (v: A),
+      ~List.In (xH, v) (xbindings m (xO i)).
+  Proof.
+    induction m; intros.
+    - simpl; auto.
+    - destruct o; simpl; intro H; destruct (in_app_or _ _ _ H).
+      + generalize H0; apply IHm1; auto.
+      + destruct (in_inv H0). congruence.
+        generalize H1; apply IHm2; auto.
+      + generalize H0; apply IHm1; auto.
+      + generalize H0; apply IHm2; auto.
+  Qed.
+
+  Lemma find_xfind_h :
+    forall (m: t A) (i: key), find i m = xfind i xH m.
+  Proof.
+    destruct i; simpl; auto.
+  Qed.
+
+  Lemma xbindings_complete:
+    forall (i j : key) (m: t A) (v: A),
+      List.In (i, v) (xbindings m j) -> xfind i j m = Some v.
+  Proof.
+      induction i; simpl; intros; destruct j; simpl.
+       apply IHi; apply xbindings_ii; auto.
+       absurd (List.In (xI i, v) (xbindings m (xO j))); auto; apply xbindings_io.
+       destruct m.
+        simpl in H; tauto.
+        rewrite find_xfind_h. apply IHi. apply (xbindings_ih _ _ _ _ _ H).
+       absurd (List.In (xO i, v) (xbindings m (xI j))); auto; apply xbindings_oi.
+       apply IHi; apply xbindings_oo; auto.
+       destruct m.
+        simpl in H; tauto.
+        rewrite find_xfind_h. apply IHi. apply (xbindings_oh _ _ _ _ _ H).
+       absurd (List.In (xH, v) (xbindings m (xI j))); auto; apply xbindings_hi.
+       absurd (List.In (xH, v) (xbindings m (xO j))); auto; apply xbindings_ho.
+       destruct m.
+        simpl in H; tauto.
+        destruct o; simpl in H; destruct (in_app_or _ _ _ H).
+         absurd (List.In (xH, v) (xbindings m1 (xO xH))); auto; apply xbindings_ho.
+         destruct (in_inv H0).
+          congruence.
+          absurd (List.In (xH, v) (xbindings m2 (xI xH))); auto; apply xbindings_hi.
+         absurd (List.In (xH, v) (xbindings m1 (xO xH))); auto; apply xbindings_ho.
+         absurd (List.In (xH, v) (xbindings m2 (xI xH))); auto; apply xbindings_hi.
+  Qed.
+
+  Theorem bindings_complete:
+    forall (m: t A) (i: key) (v: A),
+    List.In (i, v) (bindings m) -> find i m = Some v.
+  Proof.
+    intros m i v H.
+    unfold bindings in H.
+    rewrite find_xfind_h.
+    exact (xbindings_complete i xH m v H).
+  Qed.
+
+  Lemma cardinal_spec :
+   forall (m: t A), cardinal m = length (bindings m).
+  Proof.
+   unfold bindings.
+   intros m; set (p:=1); clearbody p; revert m p.
+   induction m; simpl; auto; intros.
+   rewrite (IHm1 (append p 2)), (IHm2 (append p 3)); auto.
+   destruct o; rewrite app_length; simpl; auto.
+  Qed.
+
+  Definition MapsTo (i:key)(v:A)(m:t A) := find i m = Some v.
+
+  Definition In (i:key)(m:t A) := exists e:A, MapsTo i e m.
+
+  Definition eq_key (p p':key*A) := E.eq (fst p) (fst p').
+
+  Definition eq_key_elt (p p':key*A) :=
+          E.eq (fst p) (fst p') /\ (snd p) = (snd p').
+
+  Definition lt_key (p p':key*A) := E.lt (fst p) (fst p').
+
+  Global Instance eqk_equiv : Equivalence eq_key := _.
+  Global Instance eqke_equiv : Equivalence eq_key_elt := _.
+  Global Instance ltk_strorder : StrictOrder lt_key := _.
+
+  Lemma mem_find :
+    forall m x, mem x m = match find x m with None => false | _ => true end.
+  Proof.
+  induction m; destruct x; simpl; auto.
+  Qed.
+
+  Lemma mem_spec : forall m x, mem x m = true <-> In x m.
+  Proof.
+  unfold In, MapsTo; intros m x; rewrite mem_find.
+  split.
+  - destruct (find x m).
+    exists a; auto.
+    intros; discriminate.
+  - destruct 1 as (e0,H0); rewrite H0; auto.
+  Qed.
+
+  Variable  m m' m'' : t A.
+  Variable x y z : key.
+  Variable e e' : A.
+
+  Lemma MapsTo_compat : Proper (E.eq==>eq==>eq==>iff) MapsTo.
+  Proof.
+   intros k1 k2 Hk e1 e2 He m1 m2 Hm. red in Hk. now subst.
+  Qed.
+
+  Lemma find_spec : find x m = Some e <-> MapsTo x e m.
+  Proof. reflexivity. Qed.
+
+  Lemma is_empty_spec : is_empty m = true <-> forall k, find k m = None.
+  Proof.
+  induction m; simpl.
+  - intuition. apply empty_spec.
+  - destruct o. split; try discriminate.
+    intros H. now specialize (H xH).
+    rewrite <- andb_lazy_alt, andb_true_iff, IHt0_1, IHt0_2.
+    clear IHt0_1 IHt0_2.
+    split.
+    + intros (H1,H2) k. destruct k; simpl; auto.
+    + intros H; split; intros k. apply (H (xO k)). apply (H (xI k)).
+  Qed.
+
+  Lemma bindings_spec1 :
+     InA eq_key_elt (x,e) (bindings m) <-> MapsTo x e m.
+  Proof.
+  unfold MapsTo.
+  rewrite InA_alt.
+  split.
+  - intros ((e0,a),(H,H0)).
+    red in H; simpl in H; unfold E.eq in H; destruct H; subst.
+    apply bindings_complete; auto.
+  - intro H.
+    exists (x,e).
+    split.
+    red; simpl; unfold E.eq; auto.
+    apply bindings_correct; auto.
+  Qed.
+
+  Lemma xbindings_bits_lt_1 : forall p p0 q m v,
+     List.In (p0,v) (xbindings m (append p (xO q))) -> E.bits_lt p0 p.
+  Proof.
+  intros.
+  generalize (xbindings_complete _ _ _ _ H); clear H; intros.
+  revert p0 q m v H.
+  induction p; destruct p0; simpl; intros; eauto; try discriminate.
+  Qed.
+
+  Lemma xbindings_bits_lt_2 : forall p p0 q m v,
+     List.In (p0,v) (xbindings m (append p (xI q))) -> E.bits_lt p p0.
+  Proof.
+  intros.
+  generalize (xbindings_complete _ _ _ _ H); clear H; intros.
+  revert p0 q m v H.
+  induction p; destruct p0; simpl; intros; eauto; try discriminate.
+  Qed.
+
+  Lemma xbindings_sort : forall p, sort lt_key (xbindings m p).
+  Proof.
+  induction m.
+  simpl; auto.
+  destruct o; simpl; intros.
+  (* Some *)
+  apply (SortA_app (eqA:=eq_key_elt)); auto with *.
+  constructor; auto.
+  apply In_InfA; intros.
+  destruct y0.
+  red; red; simpl.
+  eapply xbindings_bits_lt_2; eauto.
+  intros x0 y0.
+  do 2 rewrite InA_alt.
+  intros (y1,(Hy1,H)) (y2,(Hy2,H0)).
+  destruct y1; destruct x0; compute in Hy1; destruct Hy1; subst.
+  destruct y2; destruct y0; compute in Hy2; destruct Hy2; subst.
+  red; red; simpl.
+  destruct H0.
+  injection H0; clear H0; intros _ H0; subst.
+  eapply xbindings_bits_lt_1; eauto.
+  apply E.bits_lt_trans with p.
+  eapply xbindings_bits_lt_1; eauto.
+  eapply xbindings_bits_lt_2; eauto.
+  (* None *)
+  apply (SortA_app (eqA:=eq_key_elt)); auto with *.
+  intros x0 y0.
+  do 2 rewrite InA_alt.
+  intros (y1,(Hy1,H)) (y2,(Hy2,H0)).
+  destruct y1; destruct x0; compute in Hy1; destruct Hy1; subst.
+  destruct y2; destruct y0; compute in Hy2; destruct Hy2; subst.
+  red; red; simpl.
+  apply E.bits_lt_trans with p.
+  eapply xbindings_bits_lt_1; eauto.
+  eapply xbindings_bits_lt_2; eauto.
+  Qed.
+
+  Lemma bindings_spec2 : sort lt_key (bindings m).
+  Proof.
+  unfold bindings.
+  apply xbindings_sort; auto.
+  Qed.
+
+  Lemma bindings_spec2w : NoDupA eq_key (bindings m).
+  Proof.
+    apply ME.Sort_NoDupA.
+    apply bindings_spec2.
+  Qed.
+
+  (** [map] and [mapi] *)
+
+  Variable B : Type.
+
+  Section Mapi.
+
+    Variable f : key -> option A -> option B.
+
+    Fixpoint xmapi (m : t A) (i : key) : t B :=
+       match m with
+        | Leaf => Leaf
+        | Node l o r => Node (xmapi l (append i (xO xH)))
+                             (f i o)
+                             (xmapi r (append i (xI xH)))
+       end.
+
+  End Mapi.
+
+  Definition mapi (f : key -> A -> B) m :=
+    xmapi (fun k => option_map (f k)) m xH.
+
+  Definition map (f : A -> B) m := mapi (fun _ => f) m.
+
+  End A.
+
+  Lemma xgmapi:
+      forall (A B: Type) (f: key -> option A -> option B) (i j : key) (m: t A),
+        (forall k, f k None = None) ->
+        find i (xmapi f m j) = f (append j i) (find i m).
+  Proof.
+  induction i; intros; destruct m; simpl; auto.
+  rewrite (append_assoc_1 j i); apply IHi; auto.
+  rewrite (append_assoc_0 j i); apply IHi; auto.
+  rewrite append_neutral_r; auto.
+  Qed.
+
+  Theorem mapi_spec0 :
+    forall (A B: Type) (f: key -> A -> B) (i: key) (m: t A),
+    find i (mapi f m) = option_map (f i) (find i m).
+  Proof.
+  intros.
+  unfold mapi.
+  replace (f i) with (f (append xH i)).
+  apply xgmapi; auto.
+  rewrite append_neutral_l; auto.
+  Qed.
+
+  Lemma mapi_spec :
+    forall (A B: Type) (f: key -> A -> B) (m: t A) (i:key),
+    exists j, E.eq j i /\
+     find i (mapi f m) = option_map (f j) (find i m).
+  Proof.
+   intros.
+   exists i. split. reflexivity. apply mapi_spec0.
+  Qed.
+
+  Lemma map_spec :
+    forall (elt elt':Type)(f:elt->elt')(m: t elt)(x:key),
+    find x (map f m) = option_map f (find x m).
+  Proof.
+  intros; unfold map. apply mapi_spec0.
+  Qed.
+
+  Section merge.
+  Variable A B C : Type.
+  Variable f : key -> option A -> option B -> option C.
+
+  Fixpoint xmerge (m1 : t A)(m2 : t B)(i:positive) : t C :=
+    match m1 with
+    | Leaf => xmapi (fun k => f k None) m2 i
+    | Node l1 o1 r1 =>
+        match m2 with
+        | Leaf => xmapi (fun k o => f k o None) m1 i
+        | Node l2 o2 r2 =>
+          Node (xmerge l1 l2 (append i (xO xH)))
+               (f i o1 o2)
+               (xmerge r1 r2 (append i (xI xH)))
+        end
+    end.
+
+  Lemma xgmerge: forall (i j: key)(m1:t A)(m2: t B),
+      (forall i, f i None None = None) ->
+      find i (xmerge m1 m2 j) = f (append j i) (find i m1) (find i m2).
+  Proof.
+    induction i; intros; destruct m1; destruct m2; simpl; auto;
+    rewrite ?xgmapi, ?IHi,
+    <- ?append_assoc_1, <- ?append_assoc_0,
+    ?append_neutral_l, ?append_neutral_r; auto.
+  Qed.
+
+  End merge.
+
+  Definition merge {A B C}(f:key->option A->option B->option C) m1 m2 :=
+   xmerge
+     (fun k o1 o2 => match o1,o2 with
+       | None,None => None
+       | _, _ => f k o1 o2
+      end)
+     m1 m2 xH.
+
+  Lemma merge_spec1 {A B C}(f:key->option A->option B->option C) :
+    forall m m' x,
+    In x m \/ In x m' ->
+    exists y, E.eq y x /\
+     find x (merge f m m') = f y (find x m) (find x m').
+  Proof.
+  intros. exists x. split. reflexivity.
+  unfold merge.
+  rewrite xgmerge; auto.
+  rewrite append_neutral_l.
+  rewrite <- 2 mem_spec, 2 mem_find in H.
+  destruct (find x m); simpl; auto.
+  destruct (find x m'); simpl; auto. intuition discriminate.
+  Qed.
+
+  Lemma merge_spec2 {A B C}(f:key->option A->option B->option C) :
+    forall m m' x, In x (merge f m m') -> In x m \/ In x m'.
+  Proof.
+  intros.
+  rewrite <-mem_spec, mem_find in H.
+  unfold merge in H.
+  rewrite xgmerge in H; auto.
+  rewrite append_neutral_l in H.
+  rewrite <- 2 mem_spec, 2 mem_find.
+  destruct (find x m); simpl in *; auto.
+  destruct (find x m'); simpl in *; auto.
+  Qed.
+
+  Section Fold.
+
+    Variables A B : Type.
+    Variable f : key -> A -> B -> B.
+
+    Fixpoint xfoldi (m : t A) (v : B) (i : key) :=
+      match m with
+        | Leaf => v
+        | Node l (Some x) r =>
+          xfoldi r (f i x (xfoldi l v (append i 2))) (append i 3)
+        | Node l None r =>
+          xfoldi r (xfoldi l v (append i 2)) (append i 3)
+      end.
+
+    Lemma xfoldi_1 :
+      forall m v i,
+      xfoldi m v i = fold_left (fun a p => f (fst p) (snd p) a) (xbindings m i) v.
+    Proof.
+      set (F := fun a p => f (fst p) (snd p) a).
+      induction m; intros; simpl; auto.
+      destruct o.
+      rewrite fold_left_app; simpl.
+      rewrite <- IHm1.
+      rewrite <- IHm2.
+      unfold F; simpl; reflexivity.
+      rewrite fold_left_app; simpl.
+      rewrite <- IHm1.
+      rewrite <- IHm2.
+      reflexivity.
+    Qed.
+
+    Definition fold m i := xfoldi m i 1.
+
+  End Fold.
+
+  Lemma fold_spec :
+    forall (A:Type)(m:t A)(B:Type)(i : B) (f : key -> A -> B -> B),
+    fold f m i = fold_left (fun a p => f (fst p) (snd p) a) (bindings m) i.
+  Proof.
+    intros; unfold fold, bindings.
+    rewrite xfoldi_1; reflexivity.
+  Qed.
+
+  Fixpoint equal (A:Type)(cmp : A -> A -> bool)(m1 m2 : t A) : bool :=
+    match m1, m2 with
+      | Leaf, _ => is_empty m2
+      | _, Leaf => is_empty m1
+      | Node l1 o1 r1, Node l2 o2 r2 =>
+           (match o1, o2 with
+             | None, None => true
+             | Some v1, Some v2 => cmp v1 v2
+             | _, _ => false
+            end)
+           &&& equal cmp l1 l2 &&& equal cmp r1 r2
+     end.
+
+  Definition Equal (A:Type)(m m':t A) :=
+    forall y, find y m = find y m'.
+  Definition Equiv (A:Type)(eq_elt:A->A->Prop) m m' :=
+    (forall k, In k m <-> In k m') /\
+    (forall k e e', MapsTo k e m -> MapsTo k e' m' -> eq_elt e e').
+  Definition Equivb (A:Type)(cmp: A->A->bool) := Equiv (Cmp cmp).
+
+  Lemma equal_1 : forall (A:Type)(m m':t A)(cmp:A->A->bool),
+    Equivb cmp m m' -> equal cmp m m' = true.
+  Proof.
+  induction m.
+  - (* m = Leaf *)
+    destruct 1 as (E,_); simpl.
+    apply is_empty_spec; intros k.
+    destruct (find k m') eqn:F; trivial.
+    assert (H : In k m') by now exists a.
+    rewrite <- E in H.
+    destruct H as (x,H). red in H. now rewrite gleaf in H.
+  - (* m = Node *)
+    destruct m'.
+    + (* m' = Leaf *)
+      destruct 1 as (E,_); simpl.
+      destruct o.
+      * assert (H : In xH (@Leaf A)).
+        { rewrite <- E. now exists a. }
+        destruct H as (e,H). now red in H.
+      * apply andb_true_intro; split; apply is_empty_spec; intros k.
+        destruct (find k m1) eqn:F; trivial.
+        assert (H : In (xO k) (@Leaf A)).
+        { rewrite <- E. exists a; auto. }
+        destruct H as (x,H). red in H. now rewrite gleaf in H.
+        destruct (find k m2) eqn:F; trivial.
+        assert (H : In (xI k) (@Leaf A)).
+        { rewrite <- E. exists a; auto. }
+        destruct H as (x,H). red in H. now rewrite gleaf in H.
+    + (* m' = Node *)
+      destruct 1.
+      assert (Equivb cmp m1 m'1).
+      { split.
+        intros k; generalize (H (xO k)); unfold In, MapsTo; simpl; auto.
+        intros k e e'; generalize (H0 (xO k) e e'); unfold In, MapsTo; simpl; auto. }
+      assert (Equivb cmp m2 m'2).
+      { split.
+        intros k; generalize (H (xI k)); unfold In, MapsTo; simpl; auto.
+        intros k e e'; generalize (H0 (xI k) e e'); unfold In, MapsTo; simpl; auto. }
+      simpl.
+      destruct o; destruct o0; simpl.
+      repeat (apply andb_true_intro; split); auto.
+      apply (H0 xH); red; auto.
+      generalize (H xH); unfold In, MapsTo; simpl; intuition.
+      destruct H4; try discriminate; eauto.
+      generalize (H xH); unfold In, MapsTo; simpl; intuition.
+      destruct H5; try discriminate; eauto.
+      apply andb_true_intro; split; auto.
+  Qed.
+
+  Lemma equal_2 : forall (A:Type)(m m':t A)(cmp:A->A->bool),
+    equal cmp m m' = true -> Equivb cmp m m'.
+  Proof.
+  induction m.
+  (* m = Leaf *)
+  simpl.
+  split; intros.
+  split.
+  destruct 1; red in H0; destruct k; discriminate.
+  rewrite is_empty_spec in H.
+  intros (e,H'). red in H'. now rewrite H in H'.
+  red in H0; destruct k; discriminate.
+  (* m = Node *)
+  destruct m'.
+  (* m' = Leaf *)
+  simpl.
+  destruct o; intros; try discriminate.
+  destruct (andb_prop _ _ H); clear H.
+  split; intros.
+  split; unfold In, MapsTo; destruct 1.
+  destruct k; simpl in *; try discriminate.
+  rewrite is_empty_spec in H1.
+  now rewrite H1 in H.
+  rewrite is_empty_spec in H0.
+  now rewrite H0 in H.
+  destruct k; simpl in *; discriminate.
+  unfold In, MapsTo; destruct k; simpl in *; discriminate.
+  (* m' = Node *)
+  destruct o; destruct o0; simpl; intros; try discriminate.
+  destruct (andb_prop _ _ H); clear H.
+  destruct (andb_prop _ _ H0); clear H0.
+  destruct (IHm1 _ _ H2); clear H2 IHm1.
+  destruct (IHm2 _ _ H1); clear H1 IHm2.
+  split; intros.
+  destruct k; unfold In, MapsTo in *; simpl; auto.
+  split; eauto.
+  destruct k; unfold In, MapsTo in *; simpl in *.
+  eapply H4; eauto.
+  eapply H3; eauto.
+  congruence.
+  destruct (andb_prop _ _ H); clear H.
+  destruct (IHm1 _ _ H0); clear H0 IHm1.
+  destruct (IHm2 _ _ H1); clear H1 IHm2.
+  split; intros.
+  destruct k; unfold In, MapsTo in *; simpl; auto.
+  split; eauto.
+  destruct k; unfold In, MapsTo in *; simpl in *.
+  eapply H3; eauto.
+  eapply H2; eauto.
+  try discriminate.
+  Qed.
+
+Lemma equal_spec : forall (A:Type)(m m':t A)(cmp:A->A->bool),
+    equal cmp m m' = true <-> Equivb cmp m m'.
+Proof.
+ split. apply equal_2. apply equal_1.
+Qed.
+
+End PositiveMap.
+
+(** Here come some additionnal facts about this implementation.
+  Most are facts that cannot be derivable from the general interface. *)
+
+Module PositiveMapAdditionalFacts.
+  Import PositiveMap.
+
+  (* Derivable from the Map interface *)
+  Theorem gsspec {A} i j x (m: t A) :
+    find i (add j x m) = if E.eq_dec i j then Some x else find i m.
+  Proof.
+    destruct (E.eq_dec i j) as [->|];
+    [ apply add_spec1 | apply add_spec2; auto ].
+  Qed.
+
+   (* Not derivable from the Map interface *)
+  Theorem gsident {A} i (m:t A) v :
+    find i m = Some v -> add i v m = m.
+  Proof.
+    revert m.
+    induction i; destruct m; simpl in *; try congruence.
+    - intro H; now rewrite (IHi m2 H).
+    - intro H; now rewrite (IHi m1 H).
+  Qed.
+
+  Lemma xmapi_ext {A B}(f g: key -> option A -> option B) :
+    (forall k (o : option A), f k o = g k o) ->
+    forall m i, xmapi f m i = xmapi g m i.
+  Proof.
+    induction m; intros; simpl; auto. now f_equal.
+  Qed.
+
+  Theorem xmerge_commut{A B C}
+    (f: key -> option A -> option B -> option C)
+    (g: key -> option B -> option A -> option C) :
+    (forall k o1 o2, f k o1 o2 = g k o2 o1) ->
+    forall m1 m2 i, xmerge f m1 m2 i = xmerge g m2 m1 i.
+  Proof.
+    intros E.
+    induction m1; destruct m2; intros i; simpl; trivial; f_equal;
+    try apply IHm1_1; try apply IHm1_2; try apply xmapi_ext;
+    intros; apply E.
+  Qed.
+
+  Theorem merge_commut{A B C}
+    (f: key -> option A -> option B -> option C)
+    (g: key -> option B -> option A -> option C) :
+    (forall k o1 o2, f k o1 o2 = g k o2 o1) ->
+    forall m1 m2, merge f m1 m2 = merge g m2 m1.
+  Proof.
+    intros E m1 m2.
+    unfold merge. apply xmerge_commut.
+    intros k [x1|] [x2|]; trivial.
+  Qed.
+
+End PositiveMapAdditionalFacts.
diff --git a/theories/MMaps/MMaps.v b/theories/MMaps/MMaps.v
index 609cbffbb8..054d07225a 100644
--- a/theories/MMaps/MMaps.v
+++ b/theories/MMaps/MMaps.v
@@ -13,6 +13,4 @@ Require Export MMapInterface.
 Require Export MMapFacts.
 Require Export MMapWeakList.
 Require Export MMapList.
-(*
 Require Export MMapPositive.
-*)
\ No newline at end of file
diff --git a/theories/MMaps/vo.itarget b/theories/MMaps/vo.itarget
index a022bb8b22..d4861cb06e 100644
--- a/theories/MMaps/vo.itarget
+++ b/theories/MMaps/vo.itarget
@@ -2,4 +2,5 @@ MMapInterface.vo
 MMapFacts.vo
 MMapWeakList.vo
 MMapList.vo
+MMapPositive.vo
 MMaps.vo
diff --git a/theories/MSets/MSetPositive.v b/theories/MSets/MSetPositive.v
index 25a8c16292..8dd240f46e 100644
--- a/theories/MSets/MSetPositive.v
+++ b/theories/MSets/MSetPositive.v
@@ -16,79 +16,13 @@
    Sandrine Blazy (used for building certified compilers).
 *)
 
-Require Import Bool BinPos Orders MSetInterface.
+Require Import Bool BinPos Orders OrdersEx MSetInterface.
 
 Set Implicit Arguments.
 Local Open Scope lazy_bool_scope.
 Local Open Scope positive_scope.
 Local Unset Elimination Schemes.
 
-(** Even if [positive] can be seen as an ordered type with respect to the
-  usual order (see above), we can also use a lexicographic order over bits
-  (lower bits are considered first). This is more natural when using
-  [positive] as indexes for sets or maps (see FSetPositive and FMapPositive. *)
-
-Module PositiveOrderedTypeBits <: UsualOrderedType.
-  Definition t:=positive.
-  Include HasUsualEq <+ UsualIsEq.
-  Definition eqb := Pos.eqb.
-  Definition eqb_eq := Pos.eqb_eq.
-  Include HasEqBool2Dec.
-
-  Fixpoint bits_lt (p q:positive) : Prop :=
-   match p, q with
-   | xH, xI _ => True
-   | xH, _ => False
-   | xO p, xO q => bits_lt p q
-   | xO _, _ => True
-   | xI p, xI q => bits_lt p q
-   | xI _, _ => False
-   end.
-
-  Definition lt:=bits_lt.
-
-  Lemma bits_lt_antirefl : forall x : positive, ~ bits_lt x x.
-  Proof.
-   induction x; simpl; auto.
-  Qed.
-
-  Lemma bits_lt_trans :
-    forall x y z : positive, bits_lt x y -> bits_lt y z -> bits_lt x z.
-  Proof.
-   induction x; destruct y,z; simpl; eauto; intuition.
-  Qed.
-
-  Instance lt_compat : Proper (eq==>eq==>iff) lt.
-  Proof.
-   intros x x' Hx y y' Hy. rewrite Hx, Hy; intuition.
-  Qed.
-
-  Instance lt_strorder : StrictOrder lt.
-  Proof.
-   split; [ exact bits_lt_antirefl | exact bits_lt_trans ].
-  Qed.
-
-  Fixpoint compare x y :=
-    match x, y with
-      | x~1, y~1 => compare x y
-      | x~1, _ => Gt
-      | x~0, y~0 => compare x y
-      | x~0, _ => Lt
-      | 1, y~1 => Lt
-      | 1, 1 => Eq
-      | 1, y~0 => Gt
-    end.
-
-  Lemma compare_spec : forall x y, CompSpec eq lt x y (compare x y).
-  Proof.
-   unfold eq, lt.
-   induction x; destruct y; try constructor; simpl; auto.
-    destruct (IHx y); subst; auto.
-    destruct (IHx y); subst; auto.
-  Qed.
-
-End PositiveOrderedTypeBits.
-
 Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
 
   Module E:=PositiveOrderedTypeBits.
@@ -303,12 +237,6 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
       | Node l true r => S (cardinal l + cardinal r)
     end.
 
-  Definition omap (f: elt -> elt) x :=
-    match x with
-      | None => None
-      | Some i => Some (f i)
-    end.
-
   (** would it be more efficient to use a path like in the above functions ? *)
 
   Fixpoint choose (m: t) : option elt :=
@@ -316,7 +244,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
       | Leaf => None
       | Node l o r => if o then Some 1 else
         match choose l with
-          | None => omap xI (choose r)
+          | None => option_map xI (choose r)
           | Some i => Some i~0
         end
     end.
@@ -326,7 +254,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
       | Leaf => None
       | Node l o r =>
         match min_elt l with
-          | None => if o then Some 1 else omap xI (min_elt r)
+          | None => if o then Some 1 else option_map xI (min_elt r)
           | Some i => Some i~0
         end
     end.
@@ -336,7 +264,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
       | Leaf => None
       | Node l o r =>
         match max_elt r with
-          | None => if o then Some 1 else omap xO (max_elt l)
+          | None => if o then Some 1 else option_map xO (max_elt l)
           | Some i => Some i~1
         end
     end.
@@ -967,7 +895,6 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
   Lemma elements_spec2w: forall s, NoDupA E.eq (elements s).
   Proof.
     intro. apply SortA_NoDupA with E.lt; auto with *.
-    apply E.eq_equiv.
     apply elements_spec2.
   Qed.
 
diff --git a/theories/Structures/OrdersEx.v b/theories/Structures/OrdersEx.v
index acc7c76735..b484257b99 100644
--- a/theories/Structures/OrdersEx.v
+++ b/theories/Structures/OrdersEx.v
@@ -84,3 +84,70 @@ Module PairOrderedType(O1 O2:OrderedType) <: OrderedType.
 
 End PairOrderedType.
 
+(** Even if [positive] can be seen as an ordered type with respect to the
+  usual order (see above), we can also use a lexicographic order over bits
+  (lower bits are considered first). This is more natural when using
+  [positive] as indexes for sets or maps (see MSetPositive and MMapPositive. *)
+
+Local Open Scope positive.
+
+Module PositiveOrderedTypeBits <: UsualOrderedType.
+  Definition t:=positive.
+  Include HasUsualEq <+ UsualIsEq.
+  Definition eqb := Pos.eqb.
+  Definition eqb_eq := Pos.eqb_eq.
+  Include HasEqBool2Dec.
+
+  Fixpoint bits_lt (p q:positive) : Prop :=
+   match p, q with
+   | xH, xI _ => True
+   | xH, _ => False
+   | xO p, xO q => bits_lt p q
+   | xO _, _ => True
+   | xI p, xI q => bits_lt p q
+   | xI _, _ => False
+   end.
+
+  Definition lt:=bits_lt.
+
+  Lemma bits_lt_antirefl : forall x : positive, ~ bits_lt x x.
+  Proof.
+   induction x; simpl; auto.
+  Qed.
+
+  Lemma bits_lt_trans :
+    forall x y z : positive, bits_lt x y -> bits_lt y z -> bits_lt x z.
+  Proof.
+   induction x; destruct y,z; simpl; eauto; intuition.
+  Qed.
+
+  Instance lt_compat : Proper (eq==>eq==>iff) lt.
+  Proof.
+   intros x x' Hx y y' Hy. rewrite Hx, Hy; intuition.
+  Qed.
+
+  Instance lt_strorder : StrictOrder lt.
+  Proof.
+   split; [ exact bits_lt_antirefl | exact bits_lt_trans ].
+  Qed.
+
+  Fixpoint compare x y :=
+    match x, y with
+      | x~1, y~1 => compare x y
+      | x~1, _ => Gt
+      | x~0, y~0 => compare x y
+      | x~0, _ => Lt
+      | 1, y~1 => Lt
+      | 1, 1 => Eq
+      | 1, y~0 => Gt
+    end.
+
+  Lemma compare_spec : forall x y, CompSpec eq lt x y (compare x y).
+  Proof.
+   unfold eq, lt.
+   induction x; destruct y; try constructor; simpl; auto.
+    destruct (IHx y); subst; auto.
+    destruct (IHx y); subst; auto.
+  Qed.
+
+End PositiveOrderedTypeBits.
diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml
index 2df7c2273e..b29ba1efc5 100644
--- a/toplevel/cerrors.ml
+++ b/toplevel/cerrors.ml
@@ -52,12 +52,15 @@ let _ = Errors.register_handler explain_exn_default
 
 (** Pre-explain a vernac interpretation error *)
 
-let wrap_vernac_error (exn, info) strm =
-  let header = Pp.tag (Pp.Tag.inj Ppstyle.error_tag Ppstyle.tag) (str "Error:") in
-  let e = EvaluatedError (hov 0 (header ++ spc () ++ strm), None) in
-  (e, info)
+let wrap_vernac_error with_header (exn, info) strm =
+  if with_header then
+    let header = Pp.tag (Pp.Tag.inj Ppstyle.error_tag Ppstyle.tag) (str "Error:") in
+    let e = EvaluatedError (hov 0 (header ++ spc () ++ strm), None) in
+    (e, info)
+  else
+    (EvaluatedError (strm, None), info)
 
-let process_vernac_interp_error exn = match fst exn with
+let process_vernac_interp_error with_header exn = match fst exn with
   | Univ.UniverseInconsistency i ->
     let msg =
       if !Constrextern.print_universes then
@@ -65,40 +68,40 @@ let process_vernac_interp_error exn = match fst exn with
 	  Univ.explain_universe_inconsistency Universes.pr_with_global_universes i
       else
 	mt() in
-    wrap_vernac_error exn (str "Universe inconsistency" ++ msg ++ str ".")
+    wrap_vernac_error with_header exn (str "Universe inconsistency" ++ msg ++ str ".")
   | TypeError(ctx,te) ->
-      wrap_vernac_error exn (Himsg.explain_type_error ctx Evd.empty te)
+      wrap_vernac_error with_header exn (Himsg.explain_type_error ctx Evd.empty te)
   | PretypeError(ctx,sigma,te) ->
-      wrap_vernac_error exn (Himsg.explain_pretype_error ctx sigma te)
+      wrap_vernac_error with_header exn (Himsg.explain_pretype_error ctx sigma te)
   | Typeclasses_errors.TypeClassError(env, te) ->
-      wrap_vernac_error exn (Himsg.explain_typeclass_error env te)
+      wrap_vernac_error with_header exn (Himsg.explain_typeclass_error env te)
   | InductiveError e ->
-      wrap_vernac_error exn (Himsg.explain_inductive_error e)
+      wrap_vernac_error with_header exn (Himsg.explain_inductive_error e)
   | Modops.ModuleTypingError e ->
-      wrap_vernac_error exn (Himsg.explain_module_error e)
+      wrap_vernac_error with_header exn (Himsg.explain_module_error e)
   | Modintern.ModuleInternalizationError e ->
-      wrap_vernac_error exn (Himsg.explain_module_internalization_error e)
+      wrap_vernac_error with_header exn (Himsg.explain_module_internalization_error e)
   | RecursionSchemeError e ->
-      wrap_vernac_error exn (Himsg.explain_recursion_scheme_error e)
+      wrap_vernac_error with_header exn (Himsg.explain_recursion_scheme_error e)
   | Cases.PatternMatchingError (env,sigma,e) ->
-      wrap_vernac_error exn (Himsg.explain_pattern_matching_error env sigma e)
+      wrap_vernac_error with_header exn (Himsg.explain_pattern_matching_error env sigma e)
   | Tacred.ReductionTacticError e ->
-      wrap_vernac_error exn (Himsg.explain_reduction_tactic_error e)
+      wrap_vernac_error with_header exn (Himsg.explain_reduction_tactic_error e)
   | Logic.RefinerError e ->
-      wrap_vernac_error exn (Himsg.explain_refiner_error e)
+      wrap_vernac_error with_header exn (Himsg.explain_refiner_error e)
   | Nametab.GlobalizationError q ->
-      wrap_vernac_error exn
+      wrap_vernac_error with_header exn
         (str "The reference" ++ spc () ++ Libnames.pr_qualid q ++
 	 spc () ++ str "was not found" ++
 	 spc () ++ str "in the current" ++ spc () ++ str "environment.")
   | Refiner.FailError (i,s) ->
       let s = Lazy.force s in
-      wrap_vernac_error exn
+      wrap_vernac_error with_header exn
 	(str "Tactic failure" ++
          (if Pp.is_empty s then s else str ": " ++ s) ++
          if Int.equal i 0 then str "." else str " (level " ++ int i ++ str").")
   | AlreadyDeclared msg ->
-      wrap_vernac_error exn (msg ++ str ".")
+      wrap_vernac_error with_header exn (msg ++ str ".")
   | _ ->
       exn
 
@@ -107,9 +110,9 @@ let rec strip_wrapping_exceptions = function
     strip_wrapping_exceptions e
   | exc -> exc
 
-let process_vernac_interp_error (exc, info) =
+let process_vernac_interp_error ?(with_header=true) (exc, info) =
   let exc = strip_wrapping_exceptions exc in
-  let e = process_vernac_interp_error (exc, info) in
+  let e = process_vernac_interp_error with_header (exc, info) in
   let ltac_trace = Exninfo.get info Proof_type.ltac_trace_info in
   let loc = Option.default Loc.ghost (Loc.get_loc info) in
   match ltac_trace with
diff --git a/toplevel/cerrors.mli b/toplevel/cerrors.mli
index 1768af118c..100b3772cc 100644
--- a/toplevel/cerrors.mli
+++ b/toplevel/cerrors.mli
@@ -12,7 +12,7 @@ val print_loc : Loc.t -> Pp.std_ppcmds
 
 (** Pre-explain a vernac interpretation error *)
 
-val process_vernac_interp_error : Util.iexn -> Util.iexn
+val process_vernac_interp_error : ?with_header:bool -> Util.iexn -> Util.iexn
 
 (** General explain function. Should not be used directly now,
     see instead function [Errors.print] and variants *)
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 1b8fdd8aed..52b4dc8cf6 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -2062,7 +2062,7 @@ let locate_if_not_already loc (e, info) =
   | Some l -> if Loc.is_ghost l then (e, Loc.add_loc info loc) else (e, info)
 
 exception HasNotFailed
-exception HasFailed of string
+exception HasFailed of std_ppcmds
 
 let with_fail b f =
   if not b then f ()
@@ -2077,8 +2077,8 @@ let with_fail b f =
            | HasNotFailed as e -> raise e
            | e ->
               let e = Errors.push e in
-              raise (HasFailed (Pp.string_of_ppcmds
-              (Errors.iprint (Cerrors.process_vernac_interp_error e)))))
+              raise (HasFailed (Errors.iprint
+                (Cerrors.process_vernac_interp_error ~with_header:false e))))
         ()
     with e when Errors.noncritical e -> 
       let (e, _) = Errors.push e in
@@ -2087,8 +2087,7 @@ let with_fail b f =
           errorlabstrm "Fail" (str "The command has not failed!")
       | HasFailed msg ->
           if is_verbose () || !Flags.ide_slave then msg_info
-    	(str "The command has indeed failed with message:" ++
-    	 fnl () ++ str "=> " ++ hov 0 (str msg))
+            (str "The command has indeed failed with message:" ++ fnl () ++ msg)
       | _ -> assert false
   end