From e3cefca41b568b1e517313051a111b0416cd2594 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 21 Nov 2015 00:16:34 +0100
Subject: Slight simplification of the code of primitive projection (in
 relation to c71aa6b and 6ababf) so as to rely on generic functions rather
 than re-doing the de Bruijn indices cooking locally.

---
 kernel/indtypes.ml | 12 +++---------
 1 file changed, 3 insertions(+), 9 deletions(-)

(limited to 'kernel')

diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 21d1e71344..a649ec81e8 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -695,18 +695,12 @@ let compute_projections ((kn, _ as ind), u as indu) n x nparamargs params
       that typechecking projections requires just a substitution and not
       matching with a parameter context. *)
   let indty, paramsletsubst =
-    let _, _, subst, inst =
-      List.fold_right
-	(fun (na, b, t) (i, j, subst, inst) ->
-	 match b with
-	 | None -> (i-1, j-1, mkRel i :: subst, mkRel j :: inst)
-	 | Some b -> (i, j-1, substl subst b :: subst, inst))
-	paramslet (nparamargs, List.length paramslet, [], [])
-    in
+    let inst = extended_rel_list 0 paramslet in
+    let subst = subst_of_rel_context_instance paramslet inst in
     let subst = (* For the record parameter: *)
       mkRel 1 :: List.map (lift 1) subst
     in
-    let ty = mkApp (mkIndU indu, CArray.rev_of_list inst) in
+    let ty = mkApp (mkIndU indu, Array.of_list inst) in
       ty, subst
   in
   let ci = 
-- 
cgit v1.2.3