diff options
Diffstat (limited to 'interp/constrextern.ml')
| -rw-r--r-- | interp/constrextern.ml | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index a3410544e..6a893bde6 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -26,7 +26,6 @@ open Glob_ops open Pattern open Nametab open Notation -open Reserve open Detyping open Misctypes open Decl_kinds |