+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 =