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 /kernel/mod_typing.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 'kernel/mod_typing.ml')
| -rw-r--r-- | kernel/mod_typing.ml | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index b8162340f..a384c836c 100644 --- a/kernel/mod_typing.ml +++ b/kernel/mod_typing.ml @@ -167,14 +167,14 @@ and check_with_aux_mod env sign with_decl mp equiv = in let mb_mp1 = (lookup_module mp1 env) in let mtb_mp1 = - module_type_of_module env' None mb_mp1 in + module_type_of_module None mb_mp1 in let cst = match old.mod_expr with None -> begin try union_constraints (check_subtypes env' mtb_mp1 - (module_type_of_module env' None old)) + (module_type_of_module None old)) old.mod_constraints with Failure _ -> error_incorrect_with_constraint (label_of_id id) end @@ -183,8 +183,8 @@ and check_with_aux_mod env sign with_decl mp equiv = old.mod_constraints | _ -> error_generative_module_expected l in - let new_mb = strengthen_and_subst_mb mb_mp1 - (MPdot(mp,l)) env false in + let new_mb = strengthen_and_subst_mb mb_mp1 (MPdot(mp,l)) false + in let new_spec = SFBmodule {new_mb with mod_mp = MPdot(mp,l); mod_expr = Some (SEBident mp1); @@ -279,7 +279,7 @@ and translate_apply env inl ftrans mexpr mkalg = try path_of_mexpr mexpr with Not_path -> error_application_to_not_path mexpr in - let mtb = module_type_of_module env None (lookup_module mp1 env) in + let mtb = module_type_of_module None (lookup_module mp1 env) in let cst2 = check_subtypes env mtb farg_b in let mp_delta = discr_resolver env mtb in let mp_delta = inline_delta_resolver env inl mp1 farg_id farg_b mp_delta in @@ -303,7 +303,7 @@ and translate_functor env inl arg_id arg_e trans mkalg = and translate_struct_module_entry env mp inl = function | MSEident mp1 -> let mb = lookup_module mp1 env in - let mb' = strengthen_and_subst_mb mb mp env false in + let mb' = strengthen_and_subst_mb mb mp false in mb'.mod_type, Some (SEBident mp1), mb'.mod_delta,Univ.empty_constraint | MSEfunctor (arg_id, arg_e, body_expr) -> let trans env' = translate_struct_module_entry env' mp inl body_expr in @@ -345,13 +345,13 @@ and translate_module_type env mp inl mte = typ_expr = sign; typ_expr_alg = None; typ_constraints = cst; - typ_delta = resolve} mp env + typ_delta = resolve} mp in {mtb with typ_expr_alg = alg} let rec translate_struct_include_module_entry env mp inl = function | MSEident mp1 -> let mb = lookup_module mp1 env in - let mb' = strengthen_and_subst_mb mb mp env true in + let mb' = strengthen_and_subst_mb mb mp true in let mb_typ = clean_bounded_mod_expr mb'.mod_type in mb_typ,None,mb'.mod_delta,Univ.empty_constraint | MSEapply (fexpr,mexpr) -> |