From 2bb2d480b547e58deb2ec62791c8990ecac777b0 Mon Sep 17 00:00:00 2001
From: filliatr
Date: Tue, 10 Apr 2001 13:21:45 +0000
Subject: réparation Correctness; options Extraction (changement de syntaxe)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1571 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/reduction.ml | 12 ++++++++----
 1 file changed, 8 insertions(+), 4 deletions(-)

(limited to 'kernel/reduction.ml')

diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index fa2384d47d..72f577a7cc 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -1008,15 +1008,19 @@ let hnf env sigma c = apprec env sigma (c, empty_stack)
 
 (* A reduction function like whd_betaiota but which keeps casts
  * and does not reduce redexes containing meta-variables.
- * ASSUMES THAT APPLICATIONS ARE BINARY ONES.
- * Used in Programs.
+ * Used in Correctness.
  * Added by JCF, 29/1/98. *)
 
 let whd_programs_stack env sigma = 
   let rec whrec (x, stack as s) =
     match kind_of_term x with
-      | IsApp (f,([|c|] as cl)) ->
-	  if occur_meta c then s else whrec (f, append_stack cl stack)
+      | IsApp (f,cl) ->
+	  let n = Array.length cl - 1 in
+	  let c = cl.(n) in
+	  if occur_meta c then 
+	    s 
+	  else 
+	    whrec (mkApp (f, Array.sub cl 0 n), append_stack [|c|] stack)
       | IsLambda (_,_,c) ->
           (match decomp_stack stack with
              | None -> s
-- 
cgit v1.2.3