diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-05-17 17:30:55 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-05-17 17:30:55 +0000 |
| commit | 7386d0718f8c1e6fb47eea787d4287338f9e7060 (patch) | |
| tree | 7aebb7f48f1d724596d14a8a147e7d68f7317626 /library/declaremods.ml | |
| parent | cc5d102f0d9e3eef2e7b810c47002f26335601db (diff) | |
Modops: the strengthening functions can work without any env argument
The env was used for a particular case of Cbytegen.compile_constant_body,
but we can actually guess that it will answer a particular BCallias con.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14134 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library/declaremods.ml')
| -rw-r--r-- | library/declaremods.ml | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/library/declaremods.ml b/library/declaremods.ml index 2b29868bd..8753624a9 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -179,15 +179,14 @@ let check_sub mtb sub_mtb_l = environment. *) let check_subtypes mp sub_mtb_l = - let env = Global.env () in - let mb = Environ.lookup_module mp env in - let mtb = Modops.module_type_of_module env None mb in + let mb = Global.lookup_module mp in + let mtb = Modops.module_type_of_module None mb in check_sub mtb sub_mtb_l (* Same for module type [mp] *) let check_subtypes_mt mp sub_mtb_l = - check_sub (Environ.lookup_modtype mp (Global.env())) sub_mtb_l + check_sub (Global.lookup_modtype mp) sub_mtb_l (* Create a functor type entry *) |