diff options
Diffstat (limited to 'plugins/ltac/tacintern.mli')
| -rw-r--r-- | plugins/ltac/tacintern.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/ltac/tacintern.mli b/plugins/ltac/tacintern.mli index e3a4d5c79..8021dc715 100644 --- a/plugins/ltac/tacintern.mli +++ b/plugins/ltac/tacintern.mli @@ -47,7 +47,7 @@ val intern_constr_with_bindings : glob_sign -> constr_expr * constr_expr bindings -> glob_constr_and_expr * glob_constr_and_expr bindings -val intern_hyp : glob_sign -> Id.t Loc.located -> Id.t Loc.located +val intern_hyp : glob_sign -> lident -> lident (** Adds a globalization function for extra generic arguments *) |