From 6ababf42b3f03926c30cfbd209436ec83a21769e Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 18 Nov 2015 17:04:12 +0100
Subject: Fixing fix c71aa6b to primitive projections.

- Introduced an error: fold was counting in the wrong direction and I
  did not test it. Sorry.
- Substitution from params-with-let to params-without-let was still
  not correct.

Hopefully everything ok now. Eventually, we should use canonical
combinators for that: extended_rel_context to built the instance and
and a combinator apparently yet to define for building a substitution
contracting the let-ins.
---
 kernel/indtypes.ml | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

(limited to 'kernel')

diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 6c32626ad9..a46c33bf03 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -653,13 +653,13 @@ 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_i
-	(fun i (na, b, t) (subst, inst) ->
+    let _, _, subst, inst =
+      List.fold_right
+	(fun (na, b, t) (i, j, subst, inst) ->
 	 match b with
-	 | None -> (mkRel i :: subst, mkRel i :: inst)
-	 | Some b -> (substl subst b) :: subst, inst)
-	1 paramslet ([], [])
+	 | 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 subst = (* For the record parameter: *)
       mkRel 1 :: List.map (lift 1) subst
-- 
cgit v1.2.3