From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 24 Mar 2006 18:33:30 +0000 (+0000)
Subject: Recently introduced bug fixed in the kernel: a stack was "forgot" during
X-Git-Tag: make_still_working~7462
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=eca6985fb1ddae45b0600b5e44fd5c8f404d2842;p=helm.git

Recently introduced bug fixed in the kernel: a stack was "forgot" during
reduction of a MutCase.
---

diff --git a/helm/software/components/cic_proof_checking/cicReduction.ml b/helm/software/components/cic_proof_checking/cicReduction.ml
index 56e98775f..046ab908a 100644
--- a/helm/software/components/cic_proof_checking/cicReduction.ml
+++ b/helm/software/components/cic_proof_checking/cicReduction.ml
@@ -639,7 +639,7 @@ if List.mem uri params then debug_print (lazy "---- OK2") ;
         in
          (match decofix (reduce (k,e,ens,term,[])) with
              (k', e', ens', C.MutConstruct (_,_,j,_), []) ->
-              reduce (k, e, ens, (List.nth pl (j-1)), [])
+              reduce (k, e, ens, (List.nth pl (j-1)), s)
            | (k', e', ens', C.MutConstruct (_,_,j,_), s') ->
               let (arity, r) =
                 let o,_ =