diff options
Diffstat (limited to 'toplevel/vernacentries.ml')
| -rw-r--r-- | toplevel/vernacentries.ml | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index cd38510f3..395119083 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -30,7 +30,6 @@ open Decl_kinds open Constrexpr open Redexpr open Lemmas -open Declaremods open Misctypes open Locality |