Rename eta_expand_ind_stacks, fix the one from the checker and adapt

it to the new representation of projections and the new mind_finite
type.

3 files changed, 8 insertions, 8 deletions

diff --git a/kernel/closure.ml b/kernel/closure.ml
index d0a9ffd642..8851ea2b66 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -854,7 +854,7 @@ let rec get_parameters depth n argstk =
 	(* strip_update_shift_app only produces Zapp and Zshift items *)
 
 
-(** [eta_expand_ind_stacks env ind c s t] computes stacks correspoding 
+(** [eta_expand_ind_stack env ind c s t] computes stacks correspoding 
     to the conversion of the eta expansion of t, considered as an inhabitant 
     of ind, and the Constructor c of this inductive type applied to arguments
     s.
@@ -863,7 +863,7 @@ let rec get_parameters depth n argstk =
     @raises Not_found if the inductive is not a primitive record, or if the 
     constructor is partially applied.
  *)
-let eta_expand_ind_stacks env ind m s (f, s') =
+let eta_expand_ind_stack env ind m s (f, s') =
   let mib = lookup_mind (fst ind) env in
     match mib.Declarations.mind_record with
     | Some (projs,pbs) when Array.length projs > 0 
diff --git a/kernel/closure.mli b/kernel/closure.mli
index 8c3eb81f4e..adcf258576 100644
--- a/kernel/closure.mli
+++ b/kernel/closure.mli
@@ -187,7 +187,7 @@ val whd_val : clos_infos -> fconstr -> constr
 val whd_stack :
   clos_infos -> fconstr -> stack -> fconstr * stack
 
-(** [eta_expand_ind_stacks env ind c s t] computes stacks correspoding 
+(** [eta_expand_ind_stack env ind c s t] computes stacks correspoding 
     to the conversion of the eta expansion of t, considered as an inhabitant 
     of ind, and the Constructor c of this inductive type applied to arguments
     s.
@@ -196,7 +196,7 @@ val whd_stack :
     @raises Not_found if the inductive is not a primitive record, or if the 
     constructor is partially applied.
  *)
-val eta_expand_ind_stacks : env -> inductive -> fconstr -> stack -> 
+val eta_expand_ind_stack : env -> inductive -> fconstr -> stack -> 
    (fconstr * stack) -> stack * stack
 
 (** Conversion auxiliary functions to do step by step normalisation *)
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 78d2105ab0..ebba231654 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -434,7 +434,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
 	     | FConstruct ((ind2,j2),u2) ->
 	       (try
  	     	  let v2, v1 =
- 	     	    eta_expand_ind_stacks (info_env infos) ind2 hd2 v2 (snd appr1)
+ 	     	    eta_expand_ind_stack (info_env infos) ind2 hd2 v2 (snd appr1)
  	     	  in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
  	     	with Not_found -> raise NotConvertible)
 	     | _ -> raise NotConvertible)
@@ -447,7 +447,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
 	     match c1 with
 	     | FConstruct ((ind1,j1),u1) ->
  	       (try let v1, v2 =
-	     	      eta_expand_ind_stacks (info_env infos) ind1 hd1 v1 (snd appr2)
+	     	      eta_expand_ind_stack (info_env infos) ind1 hd1 v1 (snd appr2)
 	     	    in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
 	     	with Not_found -> raise NotConvertible)
 	     | _ -> raise NotConvertible)
@@ -472,14 +472,14 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
     | (FConstruct ((ind1,j1),u1), _) ->
       (try
     	 let v1, v2 =
-    	   eta_expand_ind_stacks (info_env infos) ind1 hd1 v1 (snd appr2)
+    	   eta_expand_ind_stack (info_env infos) ind1 hd1 v1 (snd appr2)
     	 in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
        with Not_found -> raise NotConvertible)
 
     | (_, FConstruct ((ind2,j2),u2)) ->
       (try
     	 let v2, v1 =
-    	   eta_expand_ind_stacks (info_env infos) ind2 hd2 v2 (snd appr1)
+    	   eta_expand_ind_stack (info_env infos) ind2 hd2 v2 (snd appr1)
     	 in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
        with Not_found -> raise NotConvertible)