From ed1ee239fa5380b061453d8d2e8a75ceba024b52 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 26 Mar 2007 18:05:50 +0000 Subject: [PATCH 1/1] Serious bug fixed: a variable was captured during unfolding of Fix, resulting in the context of the return type of mutually recursive definitions being lifted for each function but the first one! --- helm/software/components/cic_proof_checking/cicReduction.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/helm/software/components/cic_proof_checking/cicReduction.ml b/helm/software/components/cic_proof_checking/cicReduction.ml index bfba135cf..213aa2356 100644 --- a/helm/software/components/cic_proof_checking/cicReduction.ml +++ b/helm/software/components/cic_proof_checking/cicReduction.ml @@ -712,12 +712,12 @@ if List.mem uri params then debug_print (lazy "---- OK2") ; let leng = List.length fl in let new_env = let counter = ref 0 in - let rec build_env e = - if !counter = leng then e + let rec build_env e' = + if !counter = leng then e' else (incr counter ; build_env - ((RS.to_env (k,e,ens,C.Fix (!counter -1, fl),[]))::e)) + ((RS.to_env (k,e,ens,C.Fix (!counter -1, fl),[]))::e')) in build_env e in -- 2.39.2