From 944f62d08b7d78bcb20dd12ba138891d432b5987 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Sun, 13 May 2018 15:21:10 +0200
Subject: Exporting Fun1 within Array so that Array.Fun1 and not only
 CArray.Fun1 works.

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

(limited to 'kernel/esubst.ml')

diff --git a/kernel/esubst.ml b/kernel/esubst.ml
index 91cc64523..4b8edf63f 100644
--- a/kernel/esubst.ml
+++ b/kernel/esubst.ml
@@ -140,7 +140,7 @@ let rec comp mk_cl s1 s2 =
     | ESID _, _ -> s2
     | SHIFT(k,s), _ -> subs_shft(k, comp mk_cl s s2)
     | _, CONS(x,s') ->
-        CONS(CArray.Fun1.map (fun s t -> mk_cl(s,t)) s1 x, comp mk_cl s1 s')
+        CONS(Array.Fun1.map (fun s t -> mk_cl(s,t)) s1 x, comp mk_cl s1 s')
     | CONS(x,s), SHIFT(k,s') ->
         let lg = Array.length x in
         if k == lg then comp mk_cl s s'
-- 
cgit v1.2.3