From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001
From: Enrico Tassi <gareuselesinge@debian.org>
Date: Sun, 25 Jan 2015 14:42:51 +0100
Subject: Imported Upstream version 8.5~beta1+dfsg

---
 kernel/esubst.ml | 18 +++++++++---------
 1 file changed, 9 insertions(+), 9 deletions(-)

(limited to 'kernel/esubst.ml')

diff --git a/kernel/esubst.ml b/kernel/esubst.ml
index 5bb34253..42ca48ef 100644
--- a/kernel/esubst.ml
+++ b/kernel/esubst.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -29,14 +29,14 @@ let el_id = ELID
 let rec el_shft_rec n = function
   | ELSHFT(el,k) -> el_shft_rec (k+n) el
   | el           -> ELSHFT(el,n)
-let el_shft n el = if n = 0 then el else el_shft_rec n el
+let el_shft n el = if Int.equal n 0 then el else el_shft_rec n el
 
 (* cross n binders *)
 let rec el_liftn_rec n = function
   | ELID        -> ELID
   | ELLFT(k,el) -> el_liftn_rec (n+k) el
   | el          -> ELLFT(n, el)
-let el_liftn n el = if n = 0 then el else el_liftn_rec n el
+let el_liftn n el = if Int.equal n 0 then el else el_liftn_rec n el
 
 let el_lift el = el_liftn_rec 1 el
 
@@ -49,7 +49,7 @@ let rec reloc_rel n = function
 
 let rec is_lift_id = function
   | ELID -> true
-  | ELSHFT(e,n) -> n=0 & is_lift_id e
+  | ELSHFT(e,n) -> Int.equal n 0 && is_lift_id e
   | ELLFT (_,e) -> is_lift_id e
 
 (*********************)
@@ -73,7 +73,7 @@ type 'a subs =
 
 let subs_id i = ESID i
 
-let subs_cons(x,s) = if Array.length x = 0 then s else CONS(x,s)
+let subs_cons(x,s) = if Int.equal (Array.length x) 0 then s else CONS(x,s)
 
 let subs_liftn n = function
   | ESID p        -> ESID (p+n) (* bounded identity lifted extends by p *)
@@ -81,13 +81,13 @@ let subs_liftn n = function
   | lenv          -> LIFT (n,lenv)
 
 let subs_lift a = subs_liftn 1 a
-let subs_liftn n a = if n = 0 then a else subs_liftn n a
+let subs_liftn n a = if Int.equal n 0 then a else subs_liftn n a
 
 let subs_shft = function
   | (0, s)            -> s
   | (n, SHIFT (k,s1)) -> SHIFT (k+n, s1)
   | (n, s)            -> SHIFT (n,s)
-let subs_shft (n,a) = if n = 0 then a else subs_shft(n,a)
+let subs_shft s = if Int.equal (fst s) 0 then snd s else subs_shft s
 
 let subs_shift_cons = function
   (0, s, t)           -> CONS(t,s)
@@ -99,7 +99,7 @@ let rec is_subs_id = function
     ESID _     -> true
   | LIFT(_,s)  -> is_subs_id s
   | SHIFT(0,s) -> is_subs_id s
-  | CONS(x,s)  -> Array.length x = 0 && is_subs_id s
+  | CONS(x,s)  -> Int.equal (Array.length x) 0 && is_subs_id s
   | _          -> false
 
 (* Expands de Bruijn k in the explicit substitution subs
@@ -136,7 +136,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(Array.map (fun t -> mk_cl(s1,t)) x, comp mk_cl s1 s')
+        CONS(CArray.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