+*)
+
+ 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