diff options
| author | coq | 2002-09-27 12:10:04 +0000 |
|---|---|---|
| committer | coq | 2002-09-27 12:10:04 +0000 |
| commit | 2069ddbed501da4f24203d3fb92187e012ab582d (patch) | |
| tree | e29d9b1ec828157064f8b25e2e9167913f9f3298 /library/declaremods.ml | |
| parent | 6a9f037bad58c73aff5a972b36a2d5549ab37e71 (diff) | |
Encore quelques rangements dans Nametab + petits trucs
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3039 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library/declaremods.ml')
| -rw-r--r-- | library/declaremods.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/library/declaremods.ml b/library/declaremods.ml index 4169fa56fe..397104d7b5 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -344,6 +344,7 @@ let classify_modtype (_,(_,substobjs)) = let (in_modtype,out_modtype) = declare_object {(default_object "MODULE TYPE") with cache_function = cache_modtype; + open_function = open_modtype; load_function = load_modtype; subst_function = subst_modtype; classify_function = classify_modtype; |