diff options
Diffstat (limited to 'user-contrib/Ltac2/tac2intern.mli')
| -rw-r--r-- | user-contrib/Ltac2/tac2intern.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/user-contrib/Ltac2/tac2intern.mli b/user-contrib/Ltac2/tac2intern.mli index 5e282a386a..1caca3a411 100644 --- a/user-contrib/Ltac2/tac2intern.mli +++ b/user-contrib/Ltac2/tac2intern.mli @@ -46,3 +46,4 @@ val error_nparams_mismatch : ?loc:Loc.t -> int -> int -> 'a (** Misc *) val drop_ltac2_env : Genintern.Store.t -> Genintern.Store.t +val check_ltac2_var : ?loc:Loc.t -> Genintern.Store.t -> Id.t -> 'a glb_typexpr -> unit |