From 03606e89c1e299bf9d3f824cd68d4828e4a80b73 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 24 Mar 2006 18:33:30 +0000 Subject: [PATCH] Recently introduced bug fixed in the kernel: a stack was "forgot" during reduction of a MutCase. --- components/cic_proof_checking/cicReduction.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/components/cic_proof_checking/cicReduction.ml b/components/cic_proof_checking/cicReduction.ml index 56e98775f..046ab908a 100644 --- a/components/cic_proof_checking/cicReduction.ml +++ b/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,_ = -- 2.39.2