diff options
Diffstat (limited to 'checker/typeops.ml')
-rw-r--r-- | checker/typeops.ml | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/checker/typeops.ml b/checker/typeops.ml index f22649eb5..95753769d 100644 --- a/checker/typeops.ml +++ b/checker/typeops.ml @@ -14,7 +14,6 @@ open Cic open Term open Reduction open Type_errors -open Declarations open Inductive open Environ |