let generalize0_tac args =
if args = [] then id_tac
- else exact_tac ("",0,Ast.Appl (Ast.Implicit :: args))
+ else exact_tac ("",0,Ast.Appl (Ast.Implicit `JustOne :: args))
;;
let select0_tac ~where:(wanted,hyps,where) ~job =
let letin_tac ~where ~what:(_,_,w) name =
block_tac [
select_tac ~where ~job:(`Substexpand 1) true;
- exact_tac ("",0,Ast.LetIn((Ast.Ident (name,None),None),w,Ast.Implicit));
+ exact_tac
+ ("",0,Ast.LetIn((Ast.Ident (name,None),None),w,Ast.Implicit `JustOne));
]
;;
| _ -> assert false
in
let holes =
- HExtlib.mk_list Ast.Implicit (ity.leftno+1+ ity.consno + ity.rightno) in
+ HExtlib.mk_list (Ast.Implicit `JustOne)
+ (ity.leftno+1+ ity.consno + ity.rightno) in
let eliminator =
let _,_,w = what in
Ast.Appl(Ast.Ident(name,None)::holes @ [ w ])
[ select_tac ~where ~job:(`Substexpand 1) true;
exact_tac
("",0,
- Ast.Appl(Ast.Ident(name,None)::HExtlib.mk_list Ast.Implicit 5 @
+ Ast.Appl(Ast.Ident(name,None)::HExtlib.mk_list (Ast.Implicit `JustOne) 5@
[what]))] status
;;
block_tac
[ exact_tac
("",0,(Ast.Binder (`Lambda,
- (Ast.Ident (name,None),None),Ast.Implicit)));
+ (Ast.Ident (name,None),None),Ast.Implicit `JustOne)));
if name = "_" then clear_tac [name] else id_tac ]
;;