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.

---
 proofs/logic.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'proofs')

diff --git a/proofs/logic.ml b/proofs/logic.ml
index 4934afa837..218b2671ec 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -481,7 +481,7 @@ and mk_arggoals sigma goal goalacc funty allargs =
       let env = Goal.V82.env sigma goal in
       raise (RefinerError (env,sigma,CannotApply (t, harg)))
   in
-  Array.smartfoldmap foldmap (goalacc, funty, sigma) allargs
+  Array.Smart.fold_left_map foldmap (goalacc, funty, sigma) allargs
 
 and mk_casegoals sigma goal goalacc p c =
   let env = Goal.V82.env sigma goal 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.

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

(limited to 'proofs')

diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index 6fb4119387..a75711baec 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -92,9 +92,9 @@ let cache_strategy (_,str) =
 
 let subst_strategy (subs,(local,obj)) =
   local,
-  List.smartmap
+  List.Smart.map
     (fun (k,ql as entry) ->
-      let ql' = List.smartmap (Mod_subst.subst_evaluable_reference subs) ql in
+      let ql' = List.Smart.map (Mod_subst.subst_evaluable_reference subs) ql in
       if ql==ql' then entry else (k,ql'))
     obj
 
-- 
cgit v1.2.3