let status, instance =
mk_meta status newgoalctx (`Decl newgoalty) `IsTerm
in
- instantiate ~refine:false status goal instance)
+ instantiate ~refine:false status goal instance)
;;
let select_tac ~where:((txt,txtlen,(wanted,hyps,path)) as where) ~job
in
let eliminator =
let _,_,w = what in
- Ast.Appl [ Ast.Ident (name,None) ; Ast.Implicit `Vector ; w ]
+ Ast.Appl [ Ast.Ident (name,None) ; Ast.Implicit `Vector ; w ; Ast.Implicit `Vector]
in
exact_tac ("",0,eliminator) status) ])
;;