- analyze_indty_tac ~what:t1 indtyinfo;
- sort_of_goal_tac sort;
- (fun status ->
- let ity = HExtlib.unopt !indtyinfo in
- let NReference.Ref (uri, _) = ref_of_indtyinfo ity in
- let name =
- NUri.name_of_uri uri ^ "_" ^
- snd (NCicElim.ast_of_sort
- (match !sort with NCic.Sort x -> x | _ -> assert false))
- in
- let eliminator =
- let l = [Ast.Ident (name,None); Ast.Implicit `JustOne] in
- (* Generating as many implicits as open goals *)
- let l = l @ HExtlib.mk_list (Ast.Implicit `JustOne) ity.consno in
- let _,_,t1 = t1 in
- let l = l @ [t1] in
- Ast.Appl l
- in
- cl := ity.cl;
- exact_tac ("",0,eliminator) status);
- add_names_to_goals_tac cl; dot_tac] status)
+ analyze_indty_tac ~what:t1 indtyinfo;
+ sort_of_goal_tac sort;
+ (fun status ->
+ let ity = HExtlib.unopt !indtyinfo in
+ let NReference.Ref (uri, _) = ref_of_indtyinfo ity in
+ let name =
+ NUri.name_of_uri uri ^ "_" ^
+ snd (NCicElim.ast_of_sort
+ (match !sort with NCic.Sort x -> x | _ -> assert false))
+ in
+ let eliminator =
+ let l = [Ast.Ident (name,None); Ast.Implicit `JustOne] in
+ (* Generating as many implicits as open goals *)
+ let l = l @ HExtlib.mk_list (Ast.Implicit `JustOne) ity.consno in
+ let _,_,t1 = t1 in
+ let l = l @ [t1] in
+ Ast.Appl l
+ in
+ cl := ity.cl;
+ exact_tac ("",0,eliminator) status);
+ add_names_to_goals_tac cl; dot_tac] status)