let nlist = HExtlib.list_seq 0 (nargs it leftno consno) in
(* (\forall ...\forall P.\forall DH : ( ... = ... -> P). P) *)
let params = List.map (fun x -> NTactics.intro_tac ("a" ^ string_of_int x)) nlist in
- NTactics.reduce_tac ~reduction:(`Normalize true) ~where:default_pattern::
+ (* NTactics.reduce_tac ~reduction:(`Normalize true)
+ * ~where:default_pattern::*)
params @ [
NTactics.intro_tac "P";
NTactics.intro_tac "DH";
let status =
NTactics.block_tac (
- [print_tac (lazy "ci sono");
- NTactics.reduce_tac ~reduction:(`Normalize true) ~where:default_pattern
+ [print_tac (lazy "ci sono") (*;
+ NTactics.reduce_tac ~reduction:(`Normalize true) ~where:default_pattern *)
]
@ List.map (fun x -> NTactics.intro_tac x) params @
[NTactics.intro_tac "x";
| NCic.Rel var ->
cascade_select_in_ctx status ~subst:(get_subst status) context skip (var+cur_eq)
| _ -> cascade_select_in_ctx status ~subst:(get_subst status) context skip cur_eq in
+ let varname = match var with
+ | NCic.Rel var ->
+ let name,_ = List.nth context (var+cur_eq-1) in
+ HLog.warn (Printf.sprintf "destruct: trying to remove variable: %s" name);
+ [name]
+ | _ -> []
+ in
let names_to_gen = List.filter (fun n -> n <> eq_name) names_to_gen in
if (List.exists (fun x -> List.mem x skip) names_to_gen)
then oldstatus
~what:("",0,mk_id eq_name) ~where:default_pattern;
(* NTactics.reduce_tac ~reduction:(`Normalize true)
~where:default_pattern;*)
+ (* XXX: temo che la clear multipla funzioni bene soltanto se
+ * gli identificatori sono nell'ordine giusto.
+ * Per non saper né leggere né scrivere, usiamo due clear
+ * invece di una *)
NTactics.try_tac (NTactics.clear_tac [eq_name]);
+ NTactics.try_tac (NTactics.clear_tac varname);
]@
(List.map NTactics.intro_tac (List.rev names_to_gen))) status
;;
let has_cleared =
try
let _ = NTactics.find_in_context eq_name (get_ctx status' newgoal) in false
- with _ -> true in
+ with
+ | Sys.Break as e -> raise e
+ |_ -> true in
let rm_eq b l = if b then List.filter (fun x -> x <> eq_name) l else l in
let acc = rm_eq has_cleared acc in
let skip = rm_eq has_cleared skip in
let has_cleared =
try
let _ = NTactics.find_in_context eq_name (get_ctx status' newgoal) in false
- with _ -> true in
+ with
+ | Sys.Break as e -> raise e
+ | _ -> true in
let rm_eq b l = if b then List.filter (fun x -> x <> eq_name) l else l in
let acc = rm_eq has_cleared acc in
let skip = rm_eq has_cleared skip in