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