From d8851bbd50df1f77af0aabfe98bebd44fcb4aa02 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Wed, 23 May 2018 13:35:29 +0200
Subject: Moving Rtree.smart_map into Rtree.Smart.map.

---
 kernel/declareops.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel/declareops.ml')

diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index cc0b381c9..832d478b3 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -178,7 +178,7 @@ let recarg_length p j =
   let (_,cstrs) = Rtree.dest_node p in
   Array.length (snd (Rtree.dest_node cstrs.(j-1)))
 
-let subst_wf_paths sub p = Rtree.smartmap (subst_recarg sub) p
+let subst_wf_paths sub p = Rtree.Smart.map (subst_recarg sub) p
 
 (** {7 Substitution of inductive declarations } *)
 
-- 
cgit v1.2.3