diff options
| author |  barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-05-23 15:06:48 +0000 |
|---|---|---|
| committer | barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-05-23 15:06:48 +0000 |
| commit | f1686dbcad2515eee22b26b156fe51f6e9d22857 (patch) | |
| tree | 78778afec7b779635fd9b6b9b4ca3f5b07713d8a /checker/mod_checking.ml | |
| parent | b0098b7e2f0120941a3f8201788e167727476e51 (diff) | |
ported r14149 from v8.3 branch: bug in checker (redefined global)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14150 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'checker/mod_checking.ml')
| -rw-r--r-- | checker/mod_checking.ml | 21 |
1 files changed, 13 insertions, 8 deletions
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml index 285039eae..315571705 100644 --- a/checker/mod_checking.ml +++ b/checker/mod_checking.ml @@ -211,7 +211,7 @@ and check_with_aux_mod env mtb with_decl mp = SFBmodule msb -> msb | _ -> error_not_a_module l in - let _ = (lookup_module mp1 env) in () + let (_:module_body) = (lookup_module mp1 env) in () | With_module_body (_::_,mp) -> let old = match spec with SFBmodule msb -> msb @@ -236,18 +236,23 @@ and check_with_aux_mod env mtb with_decl mp = | Reduction.NotConvertible -> error_with_incorrect l and check_module_type env mty = - let _ = check_modtype env mty.typ_expr mty.typ_mp mty.typ_delta in () + let (_:struct_expr_body) = + check_modtype env mty.typ_expr mty.typ_mp mty.typ_delta in + () and check_module env mp mb = match mb.mod_expr, mb.mod_type with | None,mtb -> - let _ = check_modtype env mtb mb.mod_mp mb.mod_delta in () + let (_:struct_expr_body) = + check_modtype env mtb mb.mod_mp mb.mod_delta in () | Some mexpr, mtb when mtb==mexpr -> - let _ = check_modtype env mtb mb.mod_mp mb.mod_delta in () + let (_:struct_expr_body) = + check_modtype env mtb mb.mod_mp mb.mod_delta in () | Some mexpr, _ -> let sign = check_modexpr env mexpr mb.mod_mp mb.mod_delta in - let _ = check_modtype env mb.mod_type mb.mod_mp mb.mod_delta in + let (_:struct_expr_body) = + check_modtype env mb.mod_type mb.mod_mp mb.mod_delta in check_subtypes env {typ_mp=mp; typ_expr=sign; @@ -269,7 +274,7 @@ and check_structure_field env mp lab res = function let kn = mind_of_delta res kn in Indtypes.check_inductive env kn mib | SFBmodule msb -> - let _= check_module env (MPdot(mp,lab)) msb in + let (_:unit) = check_module env (MPdot(mp,lab)) msb in Modops.add_module msb env | SFBmodtype mty -> check_module_type env mty; @@ -299,7 +304,7 @@ and check_modexpr env mse mp_mse res = match mse with let sign = check_with env sign with_decl mp_mse in sign | SEBstruct(msb) -> - let _ = List.fold_left (fun env (lab,mb) -> + let (_:env) = List.fold_left (fun env (lab,mb) -> check_structure_field env mp_mse lab res mb) env msb in SEBstruct(msb) @@ -327,7 +332,7 @@ and check_modtype env mse mp_mse res = match mse with let sign = check_with env sign with_decl mp_mse in sign | SEBstruct(msb) -> - let _ = List.fold_left (fun env (lab,mb) -> + let (_:env) = List.fold_left (fun env (lab,mb) -> check_structure_field env mp_mse lab res mb) env msb in SEBstruct(msb) |