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.

---
 engine/eConstr.ml | 20 ++++++++++----------
 engine/termops.ml |  2 +-
 2 files changed, 11 insertions(+), 11 deletions(-)

(limited to 'engine')

diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index f14122ca1..f1530b2d1 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -339,7 +339,7 @@ let map_with_binders sigma g f l c0 = match kind sigma c0 with
     else mkLetIn (na, b', t', c')
   | App (c, al) ->
     let c' = f l c in
-    let al' = CArray.Fun1.Smart.map f l al in
+    let al' = Array.Fun1.Smart.map f l al in
     if c' == c && al' == al then c0
     else mkApp (c', al')
   | Proj (p, t) ->
@@ -347,25 +347,25 @@ let map_with_binders sigma g f l c0 = match kind sigma c0 with
     if t' == t then c0
     else mkProj (p, t')
   | Evar (e, al) ->
-    let al' = CArray.Fun1.Smart.map f l al in
+    let al' = Array.Fun1.Smart.map f l al in
     if al' == al then c0
     else mkEvar (e, al')
   | Case (ci, p, c, bl) ->
     let p' = f l p in
     let c' = f l c in
-    let bl' = CArray.Fun1.Smart.map f l bl in
+    let bl' = Array.Fun1.Smart.map f l bl in
     if p' == p && c' == c && bl' == bl then c0
     else mkCase (ci, p', c', bl')
   | Fix (ln, (lna, tl, bl)) ->
-    let tl' = CArray.Fun1.Smart.map f l tl in
+    let tl' = Array.Fun1.Smart.map f l tl in
     let l' = iterate g (Array.length tl) l in
-    let bl' = CArray.Fun1.Smart.map f l' bl in
+    let bl' = Array.Fun1.Smart.map f l' bl in
     if tl' == tl && bl' == bl then c0
     else mkFix (ln,(lna,tl',bl'))
   | CoFix(ln,(lna,tl,bl)) ->
-    let tl' = CArray.Fun1.Smart.map f l tl in
+    let tl' = Array.Fun1.Smart.map f l tl in
     let l' = iterate g (Array.length tl) l in
-    let bl' = CArray.Fun1.Smart.map f l' bl in
+    let bl' = Array.Fun1.Smart.map f l' bl in
     mkCoFix (ln,(lna,tl',bl'))
 
 let iter sigma f c = match kind sigma c with
@@ -391,9 +391,9 @@ let iter_with_full_binders sigma g f n c =
   | Prod (na,t,c) -> f n t; f (g (LocalAssum (na, t)) n) c
   | Lambda (na,t,c) -> f n t; f (g (LocalAssum (na, t)) n) c
   | LetIn (na,b,t,c) -> f n b; f n t; f (g (LocalDef (na, b, t)) n) c
-  | App (c,l) -> f n c; CArray.Fun1.iter f n l
-  | Evar (_,l) -> CArray.Fun1.iter f n l
-  | Case (_,p,c,bl) -> f n p; f n c; CArray.Fun1.iter f n bl
+  | App (c,l) -> f n c; Array.Fun1.iter f n l
+  | Evar (_,l) -> Array.Fun1.iter f n l
+  | Case (_,p,c,bl) -> f n p; f n c; Array.Fun1.iter f n bl
   | Proj (p,c) -> f n c
   | Fix (_,(lna,tl,bl)) ->
     Array.iter (f n) tl;
diff --git a/engine/termops.ml b/engine/termops.ml
index c271d9d99..053fcc3db 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -931,7 +931,7 @@ let dependent_main noevar sigma m t =
       match EConstr.kind sigma m, EConstr.kind sigma t with
 	| App (fm,lm), App (ft,lt) when Array.length lm < Array.length lt ->
 	    deprec m (mkApp (ft,Array.sub lt 0 (Array.length lm)));
-	    CArray.Fun1.iter deprec m
+            Array.Fun1.iter deprec m
 	      (Array.sub lt
 		(Array.length lm) ((Array.length lt) - (Array.length lm)))
 	| _, Cast (c,_,_) when noevar && isMeta sigma c -> ()
-- 
cgit v1.2.3