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

---
 interp/impargs.ml      |  2 +-
 interp/notation.ml     |  2 +-
 interp/notation_ops.ml | 12 ++++++------
 3 files changed, 8 insertions(+), 8 deletions(-)

(limited to 'interp')

diff --git a/interp/impargs.ml b/interp/impargs.ml
index 7e4c4ef4f..2db67c299 100644
--- a/interp/impargs.ml
+++ b/interp/impargs.ml
@@ -538,7 +538,7 @@ let subst_implicits_decl subst (r,imps as o) =
   let r' = fst (subst_global subst r) in if r==r' then o else (r',imps)
 
 let subst_implicits (subst,(req,l)) =
-  (ImplLocal,List.smartmap (subst_implicits_decl subst) l)
+  (ImplLocal,List.Smart.map (subst_implicits_decl subst) l)
 
 let impls_of_context ctx =
   let map (decl, impl) = match impl with
diff --git a/interp/notation.ml b/interp/notation.ml
index e6df7b96c..192c477be 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -741,7 +741,7 @@ let subst_arguments_scope (subst,(req,r,n,scl,cls)) =
         match subst_scope_class subst cl with
         | Some cl'  as ocl' when cl' != cl -> ocl'
         | _ -> ocl in
-  let cls' = List.smartmap subst_cl cls in
+  let cls' = List.Smart.map subst_cl cls in
   (ArgsScopeNoDischarge,r',n,scl,cls')
 
 let discharge_arguments_scope (_,(req,r,n,l,_)) =
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index dc6a103e0..eeda607e6 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -521,7 +521,7 @@ let rec subst_pat subst pat =
   | PatVar _ -> pat
   | PatCstr (((kn,i),j),cpl,n) ->
       let kn' = subst_mind subst kn
-      and cpl' = List.smartmap (subst_pat subst) cpl in
+      and cpl' = List.Smart.map (subst_pat subst) cpl in
       if kn' == kn && cpl' == cpl then pat else
         DAst.make ?loc:pat.CAst.loc @@ PatCstr (((kn',i),j),cpl',n)
 
@@ -536,7 +536,7 @@ let rec subst_notation_constr subst bound raw =
 
   | NApp (r,rl) ->
       let r' = subst_notation_constr subst bound r
-      and rl' = List.smartmap (subst_notation_constr subst bound) rl in
+      and rl' = List.Smart.map (subst_notation_constr subst bound) rl in
 	if r' == r && rl' == rl then raw else
 	  NApp(r',rl')
 
@@ -573,7 +573,7 @@ let rec subst_notation_constr subst bound raw =
 
   | NCases (sty,rtntypopt,rl,branches) ->
       let rtntypopt' = Option.smartmap (subst_notation_constr subst bound) rtntypopt
-      and rl' = List.smartmap
+      and rl' = List.Smart.map
         (fun (a,(n,signopt) as x) ->
 	  let a' = subst_notation_constr subst bound a in
 	  let signopt' = Option.map (fun ((indkn,i),nal as z) ->
@@ -581,9 +581,9 @@ let rec subst_notation_constr subst bound raw =
 	    if indkn == indkn' then z else ((indkn',i),nal)) signopt in
 	  if a' == a && signopt' == signopt then x else (a',(n,signopt')))
         rl
-      and branches' = List.smartmap
+      and branches' = List.Smart.map
                         (fun (cpl,r as branch) ->
-                           let cpl' = List.smartmap (subst_pat subst) cpl
+                           let cpl' = List.Smart.map (subst_pat subst) cpl
                            and r' = subst_notation_constr subst bound r in
                              if cpl' == cpl && r' == r then branch else
                                (cpl',r'))
@@ -610,7 +610,7 @@ let rec subst_notation_constr subst bound raw =
 
   | NRec (fk,idl,dll,tl,bl) ->
       let dll' =
-        Array.Smart.map (List.smartmap (fun (na,oc,b as x) ->
+        Array.Smart.map (List.Smart.map (fun (na,oc,b as x) ->
           let oc' =  Option.smartmap (subst_notation_constr subst bound) oc in
 	  let b' =  subst_notation_constr subst bound b in
 	  if oc' == oc && b' == b then x else (na,oc',b'))) dll in
-- 
cgit v1.2.3