Imported Upstream version 8.4~betaupstream/8.4_beta

1 files changed, 4 insertions, 13 deletions

diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml
index 802f9c58..ad33bae1 100644
--- a/pretyping/cbv.ml
+++ b/pretyping/cbv.ml
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: cbv.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
-
 open Util
 open Pp
 open Term
@@ -94,13 +92,6 @@ let rec shift_value n = function
 let shift_value n v =
   if n = 0 then v else shift_value n v
 
-let rec shift_stack n = function
-    TOP -> TOP
-  | APP(v,stk) -> APP(Array.map (shift_value n) v, shift_stack n stk)
-  | CASE(c,b,i,s,stk) -> CASE(c,b,i,subs_shft(n,s), shift_stack n stk)
-let shift_stack n stk =
-  if n = 0 then stk else shift_stack n stk
-
 (* Contracts a fixpoint: given a fixpoint and a bindings,
  * returns the corresponding fixpoint body, and the bindings in which
  * it should be evaluated: its first variables are the fixpoint bodies
@@ -299,7 +290,7 @@ and cbv_stack_term info stack env t =
         cbv_stack_term info (stack_app cargs stk) env br.(n-1)
 
     (* constructor of arity 0 in a Case -> IOTA *)
-    | (CONSTR((_,n),_), CASE(_,br,_,env,stk))
+    | (CONSTR((_,n),[||]), CASE(_,br,_,env,stk))
             when red_set (info_flags info) fIOTA ->
                     cbv_stack_term info stk env br.(n-1)
 
@@ -365,14 +356,14 @@ and cbv_norm_value info = function (* reduction under binders *)
 
 (* with profiling *)
 let cbv_norm infos constr =
-  with_stats (lazy (cbv_norm_term infos (ESID 0) constr))
+  with_stats (lazy (cbv_norm_term infos (subs_id 0) constr))
 
 type cbv_infos = cbv_value infos
 
 (* constant bodies are normalized at the first expansion *)
 let create_cbv_infos flgs env sigma =
   create
-    (fun old_info c -> cbv_stack_term old_info TOP (ESID 0) c)
+    (fun old_info c -> cbv_stack_term old_info TOP (subs_id 0) c)
     flgs
     env
     (Reductionops.safe_evar_value sigma)