diff options
Diffstat (limited to 'plugins/ltac/tacintern.mli')
| -rw-r--r-- | plugins/ltac/tacintern.mli | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/plugins/ltac/tacintern.mli b/plugins/ltac/tacintern.mli index 9146fced2d..a9f2d76e30 100644 --- a/plugins/ltac/tacintern.mli +++ b/plugins/ltac/tacintern.mli @@ -23,10 +23,8 @@ type glob_sign = Genintern.glob_sign = { extra : Genintern.Store.t; } -val fully_empty_glob_sign : glob_sign - val make_empty_glob_sign : unit -> glob_sign - (** same as [fully_empty_glob_sign], but with [Global.env()] as + (** build an empty [glob_sign] using [Global.env()] as environment *) (** Main globalization functions *) |