bug fix in injection: we have to recur on the generated premises

diff --git a/helm/software/components/tactics/discriminationTactics.ml b/helm/software/components/tactics/discriminationTactics.ml
index 27baa2b9d9d92262acb364f5e332b364233ad54f..f12e4b3f5d2c8da1da429ba14bba162914e52f70 100644 (file)
--- a/helm/software/components/tactics/discriminationTactics.ml
+++ b/helm/software/components/tactics/discriminationTactics.ml
@@ -81,10 +81,12 @@ let relocate_term map t =
       | C.Fix (i, fs) -> C.Fix (i, map_fs (List.length fs) k fs)
       | C.CoFix (i, cfs) -> C.CoFix (i, map_cfs (List.length cfs) k cfs)
    in
-   map_term 0 t
+   map_term 1 t
 
 let id n = n
 
+let comp f g n = f (g n) 
+
 (* term ha tipo t1=t2; funziona solo se t1 e t2 hanno in testa costruttori
 diversi *)
 
@@ -264,7 +266,30 @@ let pp ctx t =
   let names = List.map (function Some (n,_) -> Some n | None -> None) ctx in
   CicPp.pp t names
 
-let injection_tac ~term ~i ~continuation =
+let clear_term first_time context term =
+   let g () = if first_time then raise exn_nothingtodo else T.id_tac in
+   match term with
+      | C.Rel n -> 
+         begin match List.nth context (pred n) with
+            | Some (C.Name id, _) -> PST.clear ~hyps:[id]
+           | _                   -> assert false
+         end
+       | _      -> g ()
+
+let simpl_in_term context = function
+   | Cic.Rel i ->
+      let name = match List.nth context (pred i) with
+         | Some (Cic.Name s, Cic.Def _) -> s
+         | Some (Cic.Name s, Cic.Decl _) -> s
+         | _ -> assert false
+      in
+      RT.simpl_tac ~pattern:(None,[name,Cic.Implicit (Some `Hole)],None)
+   | _ -> raise exn_nonproj
+
+(* ~term vive nel contesto della tattica
+ * ~continuation riceve la mappa relativa
+ *)
+let rec injection_tac ~term ~i ~continuation =
  let give_name seed = function
    | C.Name _ as name -> name
    | C.Anonymous -> C.Name (incr seed; "y" ^ string_of_int !seed)
@@ -423,35 +448,22 @@ let injection_tac ~term ~i ~continuation =
           PET.mk_tactic tac
        in
        debug_print (lazy ("CUT: " ^ pp context cutted));   
+       let continuation ~map = continuation ~map:(comp succ map) in  
        PET.apply_tactic   
           (T.thens ~start: (P.cut_tac cutted)
-                   ~continuations:[continuation ~map:succ; tac term] 
+                   ~continuations:[
+                     (qnify_tac ~first_time:false ~term:(C.Rel 1) ~map:id 
+                                ~continuation);  
+                     tac term] 
          ) status
    | _ -> raise exn_noneq
  in
   PET.mk_tactic injection_tac
 
-let clear_term first_time context term =
-   let g () = if first_time then raise exn_nothingtodo else T.id_tac in
-   match term with
-      | C.Rel n -> 
-         begin match List.nth context (pred n) with
-            | Some (C.Name id, _) -> PST.clear ~hyps:[id]
-           | _                   -> assert false
-         end
-       | _      -> g ()
-
-let simpl_in_term context = function
-   | Cic.Rel i ->
-      let name = match List.nth context (pred i) with
-         | Some (Cic.Name s, Cic.Def _) -> s
-         | Some (Cic.Name s, Cic.Decl _) -> s
-         | _ -> assert false
-      in
-      RT.simpl_tac ~pattern:(None,[name,Cic.Implicit (Some `Hole)],None)
-   | _ -> raise exn_nonproj
-
-let rec qnify_tac ~first_time ~map ~term ~continuation =
+(* ~term vive nel contesto della tattica una volta ~mappato
+ * ~continuation riceve la mappa relativa
+ *)
+and qnify_tac ~first_time ~map ~term ~continuation =
  let are_convertible hd1 hd2 metasenv context = 
    fst (CR.are_convertible ~metasenv context hd1 hd2 CicUniv.empty_ugraph)
  in