From 901ff5c7cb30165ccf5a8e8d62eb3e775d3e962c Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Fri, 5 Sep 2014 16:52:38 +0200
Subject: 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.

---
 kernel/closure.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'kernel/closure.ml')

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 
-- 
cgit v1.2.3