5 files changed, 68 insertions, 12 deletions
diff --git a/theories/Init/Decimal.v b/theories/Init/Decimal.v
index 10c3baa2cd..855db8bc3f 100644
--- a/theories/Init/Decimal.v
+++ b/theories/Init/Decimal.v
@@ -156,6 +156,37 @@ Definition nztail_int d :=
   | Neg d => let (r, n) := nztail d in pair (Neg r) n
   end.
 
+(** [del_head n d] removes [n] digits at beginning of [d]
+    or returns [zero] if [d] has less than [n] digits. *)
+
+Fixpoint del_head n d :=
+  match n with
+  | O => d
+  | S n =>
+    match d with
+    | Nil => zero
+    | D0 d | D1 d | D2 d | D3 d | D4 d | D5 d | D6 d | D7 d | D8 d | D9 d =>
+      del_head n d
+    end
+  end.
+
+Definition del_head_int n d :=
+  match d with
+  | Pos d => Pos (del_head n d)
+  | Neg d => Neg (del_head n d)
+  end.
+
+(** [del_tail n d] removes [n] digits at end of [d]
+    or returns [zero] if [d] has less than [n] digits. *)
+
+Fixpoint del_tail n d := rev (del_head n (rev d)).
+
+Definition del_tail_int n d :=
+  match d with
+  | Pos d => Pos (del_tail n d)
+  | Neg d => Neg (del_tail n d)
+  end.
+
 Module Little.
 
 (** Successor of little-endian numbers *)
diff --git a/theories/Init/Prelude.v b/theories/Init/Prelude.v
index 6126d9c37d..71ba3e645d 100644
--- a/theories/Init/Prelude.v
+++ b/theories/Init/Prelude.v
@@ -43,5 +43,5 @@ Numeral Notation nat Nat.of_uint Nat.to_uint : nat_scope (abstract after 5001).
 (* Printing/Parsing of bytes *)
 Export Byte.ByteSyntaxNotations.
 
-(* Default substrings not considered by queries like SearchAbout *)
+(* Default substrings not considered by queries like Search *)
 Add Search Blacklist "_subproof" "_subterm" "Private_".
diff --git a/theories/QArith/QArith_base.v b/theories/QArith/QArith_base.v
index a7f338aec3..bd5225d9ef 100644
--- a/theories/QArith/QArith_base.v
+++ b/theories/QArith/QArith_base.v
@@ -44,13 +44,39 @@ Definition of_decimal (d:Decimal.decimal) : Q :=
   end.
 
 Definition to_decimal (q:Q) : option Decimal.decimal :=
+  (* choose between 123e-2 and 1.23, this is purely heuristic
+     and doesn't play any soundness role *)
+  let choose_exponent i ne :=
+    let i := match i with Decimal.Pos i | Decimal.Neg i => i end in
+    let li := Decimal.nb_digits i in
+    let le := Decimal.nb_digits (Nat.to_uint ne) in
+    Nat.ltb (Nat.add li le) ne in
+  (* print 123 / 100 as 123e-2 *)
+  let decimal_exponent i ne :=
+      let e := Z.to_int (Z.opp (Z.of_nat ne)) in
+      Decimal.DecimalExp i Decimal.Nil e in
+  (* print 123 / 100 as 1.23 *)
+  let decimal_dot i ne :=
+    let ai := match i with Decimal.Pos i | Decimal.Neg i => i end in
+    let ni := Decimal.nb_digits ai in
+    if Nat.ltb ne ni then
+      let i := Decimal.del_tail_int ne i in
+      let f := Decimal.del_head (Nat.sub ni ne) ai in
+      Decimal.Decimal i f
+    else
+      let z := match i with
+        | Decimal.Pos _ => Decimal.Pos (Decimal.zero)
+        | Decimal.Neg _ => Decimal.Neg (Decimal.zero) end in
+      Decimal.Decimal z (Nat.iter (Nat.sub ne ni) Decimal.D0 ai) in
   let num := Z.to_int (Qnum q) in
   let (den, e_den) := Decimal.nztail (Pos.to_uint (Qden q)) in
   match den with
   | Decimal.D1 Decimal.Nil =>
-    match Z.of_nat e_den with
-    | Z0 => Some (Decimal.Decimal num Decimal.Nil)
-    | e => Some (Decimal.DecimalExp num Decimal.Nil (Z.to_int (Z.opp e)))
+    match e_den with
+    | O => Some (Decimal.Decimal num Decimal.Nil)
+    | ne =>
+      if choose_exponent num ne then Some (decimal_exponent num ne)
+      else Some (decimal_dot num ne)
     end
   | _ => None
   end.
diff --git a/theories/Sorting/Mergesort.v b/theories/Sorting/Mergesort.v
index a761dba62d..f6a1efdd37 100644
--- a/theories/Sorting/Mergesort.v
+++ b/theories/Sorting/Mergesort.v
@@ -230,13 +230,13 @@ Proof.
     apply IHl.
 Qed.
 
-Theorem Sorted_sort : forall l, Sorted (sort l).
+Theorem LocallySorted_sort : forall l, Sorted (sort l).
 Proof.
 intro; apply Sorted_iter_merge. constructor.
 Qed.
 
-Corollary LocallySorted_sort : forall l, Sorted.Sorted leb (sort l).
-Proof. intro; eapply Sorted_LocallySorted_iff, Sorted_sort; auto. Qed.
+Corollary Sorted_sort : forall l, Sorted.Sorted leb (sort l).
+Proof. intro; eapply Sorted_LocallySorted_iff, LocallySorted_sort; auto. Qed.
 
 Theorem Permuted_sort : forall l, Permutation l (sort l).
 Proof.
@@ -245,7 +245,7 @@ Qed.
 
 Corollary StronglySorted_sort : forall l,
   Transitive leb -> StronglySorted leb (sort l).
-Proof. auto using Sorted_StronglySorted, LocallySorted_sort. Qed.
+Proof. auto using Sorted_StronglySorted, Sorted_sort. Qed.
 
 End Sort.
 
@@ -259,7 +259,7 @@ Module NatOrder <: TotalLeBool.
     | _, 0 => false
     | S x', S y' => leb x' y'
     end.
-  Infix "<=?" := leb (at level 35).
+  Infix "<=?" := leb (at level 70, no associativity).
   Theorem leb_total : forall a1 a2, a1 <=? a2 \/ a2 <=? a1.
   Proof.
     induction a1; destruct a2; simpl; auto.
@@ -269,4 +269,3 @@ End NatOrder.
 Module Import NatSort := Sort NatOrder.
 
 Example SimpleMergeExample := Eval compute in sort [5;3;6;1;8;6;0].
-
diff --git a/theories/Structures/Orders.v b/theories/Structures/Orders.v
index 6a0e7397eb..94938c1d4d 100644
--- a/theories/Structures/Orders.v
+++ b/theories/Structures/Orders.v
@@ -192,11 +192,11 @@ Module Type HasLtb (Import T:Typ).
 End HasLtb.
 
 Module Type LebNotation (T:Typ)(E:HasLeb T).
- Infix "<=?" := E.leb (at level 35).
+ Infix "<=?" := E.leb (at level 70, no associativity).
 End LebNotation.
 
 Module Type LtbNotation (T:Typ)(E:HasLtb T).
- Infix "<?" := E.ltb (at level 35).
+ Infix "<?" := E.ltb (at level 70, no associativity).
 End LtbNotation.
 
 Module Type LebSpec (T:Typ)(X:HasLe T)(Y:HasLeb T).