diff options
Diffstat (limited to 'toplevel/vernacentries.mli')
| -rw-r--r-- | toplevel/vernacentries.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/vernacentries.mli b/toplevel/vernacentries.mli index 8fb6f4668..2b6a881d4 100644 --- a/toplevel/vernacentries.mli +++ b/toplevel/vernacentries.mli @@ -51,7 +51,7 @@ val abort_refine : ('a -> unit) -> 'a -> unit;; val interp : Vernacexpr.vernac_expr -> unit -val vernac_reset_name : identifier Util.located -> unit +val vernac_reset_name : identifier Pp.located -> unit val vernac_backtrack : int -> int -> int -> unit |