(** fills a term pattern instantiating variable magics *)
val instantiate_level2:
- #NCic.status -> NotationEnv.t -> Stdpp.location -> NotationPt.term -> NotationPt.term
+ #NCic.status -> NotationEnv.t ->
+ Stdpp.location * string option * string option ->
+ NotationPt.term -> NotationPt.term