- match s with
- | NCic.Appl [_;_;_;_] ->
- (* leibniz *)
- let streicher_id = mk_id "streicherK"
- in
- let names_to_gen, _ =
- cascade_select_in_ctx status ~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 NotationPt.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;
- NotationPt.Implicit `JustOne;
- NotationPt.Implicit `JustOne;
- NotationPt.Implicit `JustOne;
- NotationPt.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 status ~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 NotationPt.UserInput)) in
- let gen_eq = NTactics.generalize_tac
- ~where:("",0,(Some (mk_appl [mk_id "jmeq_to_eq";
- NotationPt.Implicit `JustOne;
- NotationPt.Implicit `JustOne;
- NotationPt.Implicit `JustOne;
- mk_id eq_name]),[], Some NotationPt.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;
- NotationPt.Implicit `JustOne;
- NotationPt.Implicit `JustOne;
- NotationPt.Implicit `JustOne;
- NotationPt.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
+ let streicher_id = mk_id "streicherK" in
+ let names_to_gen, _ =
+ cascade_select_in_ctx status ~subst:(get_subst status) context skip cur_eq in
+ let gen_tac x = generalize0_tac (List.map mk_id x) in
+
+ match s with
+ (* jmeq *)
+ | NCic.Appl [_;_;_;_;_] ->
+ let names_to_gen = List.rev names_to_gen in
+ (*let gen_eq = NTactics.generalize_tac
+ ~where:("",0,(Some (mk_appl [mk_id "jmeq_to_eq";
+ NotationPt.Implicit `JustOne;
+ NotationPt.Implicit `JustOne;
+ NotationPt.Implicit `JustOne;
+ mk_id eq_name]),[], Some
+ NotationPt.UserInput)) in*)
+ let gen_eq = generalize0_tac
+ [mk_appl [mk_id "jmeq_to_eq";
+ NotationPt.Implicit `JustOne;
+ NotationPt.Implicit `JustOne;
+ NotationPt.Implicit `JustOne;
+ mk_id eq_name]] in
+ NTactics.block_tac ((gen_tac (List.rev 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;
+ NotationPt.Implicit `JustOne;
+ NotationPt.Implicit `JustOne;
+ NotationPt.Implicit `JustOne;
+ NotationPt.Implicit `JustOne]);
+ ] @
+ (List.map NTactics.intro_tac names_to_gen)) status
+
+ (* leibniz *)
+ | NCic.Appl [_;_;_;_] ->
+ begin
+ let names_to_gen, _ =
+ cascade_select_in_ctx status ~subst:(get_subst status) context skip cur_eq in
+ let names_to_gen = eq_name :: (List.rev names_to_gen) in
+ NTactics.block_tac ((gen_tac names_to_gen)::
+ [NTactics.clear_tac names_to_gen;
+ NTactics.apply_tac ("",0, mk_appl [streicher_id;
+ NotationPt.Implicit `JustOne;
+ NotationPt.Implicit `JustOne;
+ NotationPt.Implicit `JustOne;
+ NotationPt.Implicit `JustOne])
+ (* NTactics.reduce_tac ~reduction:(`Normalize true)
+ ~where:default_pattern *)
+ ] @
+ let names_to_intro = List.tl names_to_gen in
+ (List.map NTactics.intro_tac names_to_intro)) status
+ end
+ | _ -> assert false
+