diff options
Diffstat (limited to 'pretyping/arguments_renaming.ml')
| -rw-r--r-- | pretyping/arguments_renaming.ml | 9 |
1 files changed, 0 insertions, 9 deletions
diff --git a/pretyping/arguments_renaming.ml b/pretyping/arguments_renaming.ml index 7e281e056..f9eafd3ec 100644 --- a/pretyping/arguments_renaming.ml +++ b/pretyping/arguments_renaming.ml @@ -9,18 +9,9 @@ (*i*) open Names open Globnames -open Decl_kinds open Term -open Sign -open Evd open Environ -open Nametab -open Mod_subst -open Errors -open Util -open Pp open Libobject -open Nameops (*i*) let empty_name_table = (Refmap.empty : name list list Refmap.t) |