diff options
Diffstat (limited to 'vernac/vernacexpr.ml')
-rw-r--r-- | vernac/vernacexpr.ml | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index 9e8dfc4f8..5acac9e25 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -9,7 +9,6 @@ (************************************************************************) open Names -open Misctypes open Constrexpr open Libnames |