From 92081320b50b03d6bf296552d2cae9e4b398f1be Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 14 Sep 2006 12:38:12 +0000 Subject: [PATCH] Bug fixed in injection: lifting was not performed correctly, but it worked most of the time :-) --- components/tactics/discriminationTactics.ml | 14 ++++++++++++-- 1 file changed, 12 insertions(+), 2 deletions(-) diff --git a/components/tactics/discriminationTactics.ml b/components/tactics/discriminationTactics.ml index 9ec2d7622..4f959965a 100644 --- a/components/tactics/discriminationTactics.ml +++ b/components/tactics/discriminationTactics.ml @@ -132,6 +132,7 @@ and injection1_tac ~term ~i ~liftno = List.nth ind_type_list typeno in let i_constr_id,_ = List.nth constructor_list (consno - 1) in + let seed = ref 0 in let patterns = List.map (function (id,cty) -> @@ -144,13 +145,21 @@ and injection1_tac ~term ~i ~liftno = let binder' = match binder with C.Name b -> C.Name b - | C.Anonymous -> C.Name "y" + | C.Anonymous -> + C.Name + (incr seed; "y" ^ string_of_int !seed) in C.Lambda (binder',source,(aux target (k+1))) | _ -> +if id = i_constr_id then ( +prerr_endline ("k= " ^ string_of_int k); +prerr_endline ("paramsno= " ^ string_of_int paramsno); +prerr_endline ("nr_param_constr " ^ string_of_int (k - 1 - paramsno)); +prerr_endline ("rel= " ^ string_of_int (k - i)); +); let nr_param_constr = k - 1 - paramsno in if id = i_constr_id - then C.Rel (nr_param_constr - liftno) + then C.Rel (k - i) else S.lift (nr_param_constr + 1) t1' (* + 1 per liftare anche il lambda aggiunto esternamente al case *) in aux reduced_cty 1 ) constructor_list in @@ -231,6 +240,7 @@ let xxx = (turi,typeno,outtype,C.Rel 1,patterns)) ; t1] in +prerr_endline ("i=" ^ string_of_int i ^ "; liftno=" ^ string_of_int liftno); prerr_endline ("XXX: " ^ CicPp.ppterm xxx); prerr_endline ("WITH: " ^ CicPp.ppterm new_t1'); xxx, -- 2.39.2