+let clearid_tac ~context skip cur_eq =
+ fun status ->
+ let eq_name,(NCic.Decl s | NCic.Def (s,_)) = List.nth context (cur_eq-1) in
+ let _,ctx' = HExtlib.split_nth cur_eq context in
+ let status, s = NTacStatus.whd status ctx' (mk_cic_term ctx' s) in
+ let status, s = term_of_cic_term status s ctx' in
+ let skip = saturate_skip status context skip in
+ (*
+ let streicher_id =
+ match s with
+ | NCic.Appl [_;_;_;_] -> mk_id "streicherK"
+ | NCic.Appl [_;_;_;_;_] -> mk_id "streicherKjmeq"
+ | _ -> assert false
+ in
+ pp (lazy (Printf.sprintf "clearid: equation %s" eq_name));
+ let names_to_gen, _ =
+ cascade_select_in_ctx ~subst:(get_subst status) context cur_eq in
+ let names_to_gen = names_to_gen @ [eq_name] in
+ let gen_tac x =
+ NTactics.generalize_tac
+ ~where:("",0,(Some (mk_id x),[], Some CicNotationPt.UserInput)) in
+ NTactics.block_tac ((List.map gen_tac names_to_gen)@
+ [NTactics.clear_tac names_to_gen;
+ NTactics.apply_tac ("",0, mk_appl [streicher_id;
+ CicNotationPt.Implicit `JustOne;
+ CicNotationPt.Implicit `JustOne;
+ CicNotationPt.Implicit `JustOne;
+ CicNotationPt.Implicit `JustOne]);
+ NTactics.reduce_tac ~reduction:(`Normalize true)
+ ~where:default_pattern] @
+ (let names_to_intro =
+ match List.rev names_to_gen with
+ | [] -> []
+ | _::tl -> tl in
+ List.map NTactics.intro_tac names_to_intro)) status
+*)
+
+ pp (lazy (Printf.sprintf "clearid: equation %s" eq_name));
+ match s with
+ | NCic.Appl [_;_;_;_] ->
+ (* leibniz *)
+ let streicher_id = mk_id "streicherK"
+ in
+ let names_to_gen, _ =
+ cascade_select_in_ctx ~subst:(get_subst status) context skip cur_eq in
+ let names_to_gen = names_to_gen @ [eq_name] in
+ let gen_tac x =
+ NTactics.generalize_tac
+ ~where:("",0,(Some (mk_id x),[], Some CicNotationPt.UserInput)) in
+ NTactics.block_tac ((List.map gen_tac names_to_gen)@
+ [NTactics.clear_tac names_to_gen;
+ NTactics.apply_tac ("",0, mk_appl [streicher_id;
+ CicNotationPt.Implicit `JustOne;
+ CicNotationPt.Implicit `JustOne;
+ CicNotationPt.Implicit `JustOne;
+ CicNotationPt.Implicit `JustOne]);
+ NTactics.reduce_tac ~reduction:(`Normalize true)
+ ~where:default_pattern] @
+ (let names_to_intro =
+ match List.rev names_to_gen with
+ | [] -> []
+ | _::tl -> tl in
+ List.map NTactics.intro_tac names_to_intro)) status
+ | NCic.Appl [_;_;_;_;_] ->
+ (* JMeq *)
+ let streicher_id = mk_id "streicherK"
+ in
+ let names_to_gen, _ =
+ cascade_select_in_ctx ~subst:(get_subst status) context skip cur_eq in
+ let names_to_gen = names_to_gen (* @ [eq_name]*) in
+ let gen_tac x =
+ NTactics.generalize_tac
+ ~where:("",0,(Some (mk_id x),[], Some CicNotationPt.UserInput)) in
+ let gen_eq = NTactics.generalize_tac
+ ~where:("",0,(Some (mk_appl [mk_id "jmeq_to_eq";
+ CicNotationPt.Implicit `JustOne;
+ CicNotationPt.Implicit `JustOne;
+ CicNotationPt.Implicit `JustOne;
+ mk_id eq_name]),[], Some CicNotationPt.UserInput)) in
+ NTactics.block_tac ((List.map gen_tac names_to_gen)@gen_eq::
+ [NTactics.clear_tac names_to_gen;
+ NTactics.try_tac (NTactics.clear_tac [eq_name]);
+ NTactics.apply_tac ("",0, mk_appl [streicher_id;
+ CicNotationPt.Implicit `JustOne;
+ CicNotationPt.Implicit `JustOne;
+ CicNotationPt.Implicit `JustOne;
+ CicNotationPt.Implicit `JustOne]);
+ NTactics.reduce_tac ~reduction:(`Normalize true)
+ ~where:default_pattern] @
+ (let names_to_intro = List.rev names_to_gen in
+ List.map NTactics.intro_tac names_to_intro)) status
+ | _ -> assert false
+;;
+