From 2280477a96e19ba5060de2d48dcc8fd7c8079d22 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 13 Nov 2015 11:31:34 +0100 Subject: Imported Upstream version 8.5~beta3+dfsg --- checker/safe_typing.ml | 30 +++++++++++++++++++----------- 1 file changed, 19 insertions(+), 11 deletions(-) (limited to 'checker/safe_typing.ml') diff --git a/checker/safe_typing.ml b/checker/safe_typing.ml index 810d6e0b..81a3cc03 100644 --- a/checker/safe_typing.ml +++ b/checker/safe_typing.ml @@ -27,18 +27,26 @@ let set_engagement c = (* full_add_module adds module with universes and constraints *) let full_add_module dp mb univs digest = let env = !genv in - let env = add_constraints mb.mod_constraints env in - let env = add_constraints univs env in + let env = push_context_set ~strict:true mb.mod_constraints env in + let env = push_context_set ~strict:true univs env in let env = Modops.add_module mb env in genv := add_digest env dp digest -(* Check that the engagement expected by a library matches the initial one *) -let check_engagement env c = - match engagement env, c with - | Some ImpredicativeSet, Some ImpredicativeSet -> () - | _, None -> () - | _, Some ImpredicativeSet -> - error "Needs option -impredicative-set" +(* Check that the engagement expected by a library extends the initial one *) +let check_engagement env (expected_impredicative_set,expected_type_in_type) = + let impredicative_set,type_in_type = Environ.engagement env in + begin + match impredicative_set, expected_impredicative_set with + | PredicativeSet, ImpredicativeSet -> + Errors.error "Needs option -impredicative-set." + | _ -> () + end; + begin + match type_in_type, expected_type_in_type with + | StratifiedType, TypeInType -> + Errors.error "Needs option -type-in-type." + | _ -> () + end (* Libraries = Compiled modules *) @@ -75,8 +83,8 @@ let import file clib univs digest = check_engagement env clib.comp_enga; let mb = clib.comp_mod in Mod_checking.check_module - (add_constraints univs - (add_constraints mb.mod_constraints env)) mb.mod_mp mb; + (push_context_set ~strict:true univs + (push_context_set ~strict:true mb.mod_constraints env)) mb.mod_mp mb; stamp_library file digest; full_add_module clib.comp_name mb univs digest -- cgit v1.2.3