From fc6d0fb650f57a764af6fe9be44677a69be11980 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Thu, 19 Feb 2015 16:41:51 +0100
Subject: New function [Constr.equal_with] to compare terms up to variants of
 [kind_of_term].

To be able to write equality up to evar instantiation instantiation.

Generalises the main function of [eq] constr over the variant of [kind_of_term] it uses. It prevents some optimisation of [Array.equal] where two physically equal arrays are considered (less or) equal. But it does not seem to have appreciable effects on efficiency.
---
 lib/cArray.ml  | 28 ++++++++++++++++------------
 lib/cArray.mli |  5 +++++
 2 files changed, 21 insertions(+), 12 deletions(-)

(limited to 'lib')

diff --git a/lib/cArray.ml b/lib/cArray.ml
index 1603454304..bb1e335468 100644
--- a/lib/cArray.ml
+++ b/lib/cArray.ml
@@ -13,6 +13,7 @@ sig
   include S
   val compare : ('a -> 'a -> int) -> 'a array -> 'a array -> int
   val equal : ('a -> 'a -> bool) -> 'a array -> 'a array -> bool
+  val equal_norefl : ('a -> 'a -> bool) -> 'a array -> 'a array -> bool
   val is_empty : 'a array -> bool
   val exists : ('a -> bool) -> 'a array -> bool
   val exists2 : ('a -> 'b -> bool) -> 'a array -> 'b array -> bool
@@ -85,19 +86,22 @@ let compare cmp v1 v2 =
       in
       loop (len - 1)
 
+let equal_norefl cmp t1 t2 =
+  let len = Array.length t1 in
+  if not (Int.equal len (Array.length t2)) then false
+  else
+    let rec aux i =
+      if i < 0 then true
+      else
+        let x = uget t1 i in
+        let y = uget t2 i in
+        cmp x y && aux (pred i)
+    in
+    aux (len - 1)
+
 let equal cmp t1 t2 =
-  if t1 == t2 then true else
-    let len = Array.length t1 in
-    if not (Int.equal len (Array.length t2)) then false
-    else
-      let rec aux i =
-        if i < 0 then true
-        else
-          let x = uget t1 i in
-          let y = uget t2 i in
-          cmp x y && aux (pred i)
-      in
-      aux (len - 1)
+  if t1 == t2 then true else equal_norefl cmp t1 t2
+    
 
 let is_empty array = Int.equal (Array.length array) 0
 
diff --git a/lib/cArray.mli b/lib/cArray.mli
index 39c35e2d54..7e5c93b5da 100644
--- a/lib/cArray.mli
+++ b/lib/cArray.mli
@@ -17,6 +17,11 @@ sig
   val equal : ('a -> 'a -> bool) -> 'a array -> 'a array -> bool
   (** Lift equality to array type. *)
 
+  val equal_norefl : ('a -> 'a -> bool) -> 'a array -> 'a array -> bool
+  (** Like {!equal} but does not assume that equality is reflexive: no
+      optimisation is performed if both arrays are physically the
+      same. *)
+
   val is_empty : 'a array -> bool
   (** True whenever the array is empty. *)
 
-- 
cgit v1.2.3


From 15a3b57db10e61c9de12b5880b04b46db1494b5b Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 26 Feb 2015 14:31:25 +0100
Subject: Fixing printing of ordinals.

---
 lib/cString.ml |  9 ++++++++-
 lib/pp.ml      | 11 ++++++++++-
 2 files changed, 18 insertions(+), 2 deletions(-)

(limited to 'lib')

diff --git a/lib/cString.ml b/lib/cString.ml
index 250b7cee2d..e9006860fd 100644
--- a/lib/cString.ml
+++ b/lib/cString.ml
@@ -135,7 +135,14 @@ let plural n s = if n<>1 then s^"s" else s
 let conjugate_verb_to_be n = if n<>1 then "are" else "is"
 
 let ordinal n =
-  let s = match n mod 10 with 1 -> "st" | 2 -> "nd" | 3 -> "rd" | _ -> "th" in
+  let s =
+    if (n / 10) mod 10 = 1 then "th"
+    else match n mod 10 with
+    | 1 -> "st"
+    | 2 -> "nd"
+    | 3 -> "rd"
+    | _ -> "th"
+  in
   string_of_int n ^ s
 
 (* string parsing *)
diff --git a/lib/pp.ml b/lib/pp.ml
index cc56e5e8d7..76046a7f91 100644
--- a/lib/pp.ml
+++ b/lib/pp.ml
@@ -517,8 +517,17 @@ let pr_arg pr x = spc () ++ pr x
 let pr_opt pr = function None -> mt () | Some x -> pr_arg pr x
 let pr_opt_no_spc pr = function None -> mt () | Some x -> pr x
 
+(** TODO: merge with CString.ordinal *)
 let pr_nth n =
-  int n ++ str (match n mod 10 with 1 -> "st" | 2 -> "nd" | 3 -> "rd" | _ -> "th")
+  let s =
+    if (n / 10) mod 10 = 1 then "th"
+    else match n mod 10 with
+    | 1 -> "st"
+    | 2 -> "nd"
+    | 3 -> "rd"
+    | _ -> "th"
+  in
+  int n ++ str s
 
 (* [prlist pr [a ; ... ; c]] outputs [pr a ++ ... ++ pr c] *)
 
-- 
cgit v1.2.3