From f2ab2825077bf8344d2e55be433efb1891212589 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 23 May 2018 13:34:22 +0200
Subject: Collecting Array.smart_* functions into a module Array.Smart.

---
 kernel/univ.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'kernel/univ.ml')

diff --git a/kernel/univ.ml b/kernel/univ.ml
index 8e19fa4e52..6bcffdd457 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -853,7 +853,7 @@ struct
   let length a = Array.length a
 
   let subst_fn fn t = 
-    let t' = CArray.smartmap fn t in
+    let t' = CArray.Smart.map fn t in
       if t' == t then t else of_array t'
 
   let levels x = LSet.of_array x
@@ -890,7 +890,7 @@ let subst_instance_level s l =
   | _ -> l
 
 let subst_instance_instance s i = 
-  Array.smartmap (fun l -> subst_instance_level s l) i
+  Array.Smart.map (fun l -> subst_instance_level s l) i
 
 let subst_instance_universe s u =
   let f x = Universe.Expr.map (fun u -> subst_instance_level s u) x in
-- 
cgit v1.2.3


From 33b5074f24270c202a9922f21d445c12cc6b3b3d Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 23 May 2018 13:34:46 +0200
Subject: Collecting List.smart_* functions into a module List.Smart.

---
 kernel/univ.ml | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'kernel/univ.ml')

diff --git a/kernel/univ.ml b/kernel/univ.ml
index 6bcffdd457..9782312cae 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -456,10 +456,10 @@ struct
   let super l = 
     if is_small l then type1
     else
-      List.smartmap (fun x -> Expr.successor x) l
+      List.Smart.map (fun x -> Expr.successor x) l
 
   let addn n l =
-    List.smartmap (fun x -> Expr.addn n x) l
+    List.Smart.map (fun x -> Expr.addn n x) l
 
   let rec merge_univs l1 l2 =
     match l1, l2 with
@@ -500,7 +500,7 @@ struct
 
   let for_all = List.for_all
 
-  let smartmap = List.smartmap
+  let smart_map = List.Smart.map
 
   let map = List.map
 end
@@ -894,7 +894,7 @@ let subst_instance_instance s i =
 
 let subst_instance_universe s u =
   let f x = Universe.Expr.map (fun u -> subst_instance_level s u) x in
-  let u' = Universe.smartmap f u in
+  let u' = Universe.smart_map f u in
     if u == u' then u
     else Universe.sort u'
 
@@ -1100,7 +1100,7 @@ let subst_univs_level_level subst l =
 
 let subst_univs_level_universe subst u =
   let f x = Universe.Expr.map (fun u -> subst_univs_level_level subst u) x in
-  let u' = Universe.smartmap f u in
+  let u' = Universe.smart_map f u in
     if u == u' then u
     else Universe.sort u'
 
-- 
cgit v1.2.3