diff options
Diffstat (limited to 'vernac/obligations.mli')
| -rw-r--r-- | vernac/obligations.mli | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/vernac/obligations.mli b/vernac/obligations.mli index 11366fe91..a276f9f9a 100644 --- a/vernac/obligations.mli +++ b/vernac/obligations.mli @@ -12,7 +12,6 @@ open Evd open Names open Pp open Globnames -open Vernacexpr open Decl_kinds (** Forward declaration. *) |