-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
-;;
-