From 681ef7c2760a6c628ed4fa96b2f9b5690ac5e1c8 Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Wed, 24 Oct 2007 17:24:18 +0000
Subject: [PATCH] bug fix in injection: we have to recur on the generated
 premises

---
 components/tactics/discriminationTactics.ml | 60 ++++++++++++---------
 1 file changed, 36 insertions(+), 24 deletions(-)

diff --git a/components/tactics/discriminationTactics.ml b/components/tactics/discriminationTactics.ml
index 27baa2b9d..f12e4b3f5 100644
--- a/components/tactics/discriminationTactics.ml
+++ b/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
-- 
2.39.2