From 3e96002677226c0cdaa8f355938a76cfb37a722a Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Thu, 14 Oct 2010 17:51:11 +0200 Subject: Imported Upstream version 8.3 --- checker/declarations.ml | 2 +- checker/mod_checking.ml | 6 +++--- checker/reduction.ml | 3 ++- 3 files changed, 6 insertions(+), 5 deletions(-) (limited to 'checker') 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 -> () -- cgit v1.2.3