diff options
Diffstat (limited to 'pretyping/recordops.mli')
| -rwxr-xr-x | pretyping/recordops.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli index d3811f413..a3dd2f2a3 100755 --- a/pretyping/recordops.mli +++ b/pretyping/recordops.mli @@ -10,6 +10,7 @@ (*i*) open Names +open Nametab open Term open Classops open Libobject |