diff options
Diffstat (limited to 'pretyping/recordops.ml')
| -rw-r--r-- | pretyping/recordops.ml | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index 4f7d06e39..7c128d245 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -20,9 +20,7 @@ open Names open Globnames open Nametab open Term -open Typeops open Libobject -open Library open Mod_subst open Reductionops |