Bug fixed in injection: lifting was not performed correctly, but it worked

most of the time :-)

diff --git a/components/tactics/discriminationTactics.ml b/components/tactics/discriminationTactics.ml
index 9ec2d76221e19ffd3dc48f44374c7c1c085517fb..4f959965a149fe4a1d5f79ff8d317b6b2596cefd 100644 (file)
--- 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,