diff options
| author | letouzey | 2011-02-11 16:54:05 +0000 |
|---|---|---|
| committer | letouzey | 2011-02-11 16:54:05 +0000 |
| commit | 1e1bc1952499bf3528810f2b3e6efad76ab843d0 (patch) | |
| tree | 7a0244e8ca2b6d24d1cc8db72890999e6d005448 /kernel/safe_typing.ml | |
| parent | cb14f24943415cce8fcbf36cb7cdd87d27c60628 (diff) | |
Mod_typing: some refactoring (common parts about MSEapply and co)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13838 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/safe_typing.ml')
| -rw-r--r-- | kernel/safe_typing.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 52a162bd44..66c731a9de 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -444,8 +444,8 @@ let end_module l restype senv = let add_include me is_module inl senv = let sign,cst,resolver = if is_module then - let sign,resolver,cst = - translate_struct_include_module_entry senv.env + let sign,_,resolver,cst = + translate_struct_include_module_entry senv.env senv.modinfo.modpath inl me in sign,cst,resolver else |