diff options
| author |  Stephane Glondu <steph@glondu.net> | 2010-10-14 17:51:11 +0200 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2010-10-14 17:51:11 +0200 |
| commit | 3e96002677226c0cdaa8f355938a76cfb37a722a (patch) | |
| tree | 3ca96e142fdb68e464d2f5f403f315282b94f922 /checker | |
| parent | f18e6146f4fd6ed5b8ded10a3e602f5f64f919f4 (diff) | |
Imported Upstream version 8.3upstream/8.3
Diffstat (limited to 'checker')
| -rw-r--r-- | checker/declarations.ml | 2 | ||||
| -rw-r--r-- | checker/mod_checking.ml | 6 | ||||
| -rw-r--r-- | checker/reduction.ml | 3 |
3 files changed, 6 insertions, 5 deletions
diff --git a/checker/declarations.ml b/checker/declarations.ml index 699f6c90..0deb80a2 100644 --- a/checker/declarations.ml +++ b/checker/declarations.ml @@ -580,7 +580,7 @@ let update_delta_resolver resolver1 resolver2 = Equiv (solve_delta_kn resolver2 kn) in Deltamap.add key new_hint res | _ -> Deltamap.add key hint res - with not_found -> + with Not_found -> Deltamap.add key hint res in Deltamap.fold apply_res resolver1 empty_delta_resolver diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml index 23ba4893..81154cba 100644 --- a/checker/mod_checking.ml +++ b/checker/mod_checking.ml @@ -238,15 +238,15 @@ 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 in () + let _ = 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 in () + let _ = 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 in () + let _ = 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 diff --git a/checker/reduction.ml b/checker/reduction.ml index 9f7dec28..d040c3db 100644 --- a/checker/reduction.ml +++ b/checker/reduction.ml @@ -154,7 +154,8 @@ type conv_pb = let sort_cmp univ pb s0 s1 = match (s0,s1) with - | (Prop c1, Prop c2) -> if c1 = Pos & c2 = Null then raise NotConvertible + | (Prop c1, Prop c2) when pb = CUMUL -> if c1 = Pos & c2 = Null then raise NotConvertible + | (Prop c1, Prop c2) -> if c1 <> c2 then raise NotConvertible | (Prop c1, Type u) -> (match pb with CUMUL -> () |