Suppression StronglyClassical, StronglyConstructive devient plus concretement ImpredicativeSet

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4828 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 3 insertions, 16 deletions

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 5dc9883285..d007af08eb 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -409,25 +409,12 @@ let add_constraints cst senv =
 (* Check that the engagement expected by a library matches the initial one *)
 let check_engagement env c =
   match Environ.engagement env, c with
-    | Some StronglyClassical, Some StronglyClassical -> ()
-    | Some StronglyConstructive, Some StronglyConstructive -> ()
+    | Some ImpredicativeSet, Some ImpredicativeSet -> ()
     | _, None -> ()
-    | _, Some StronglyClassical ->
-        error "Needs option -strongly-classical"
-    | _, Some StronglyConstructive ->
-        error "Needs option -strongly-classical"
-
-(* Check the initial engagement (possibly after a state input) *)
-let check_initial_engagement env c =
-  match Environ.engagement env, c with
-    | Some StronglyConstructive, StronglyClassical ->
-        error "Already engaged for a strongly constructive logic"
-    | Some StronglyClassical, StronglyConstructive ->
-        error "Already engaged for a strongly classical logic"
-    | _ -> ()
+    | _, Some ImpredicativeSet ->
+        error "Needs option -impredicative-set"
 
 let set_engagement c senv =
-  check_initial_engagement senv.env c;
   {senv with env = Environ.set_engagement c senv.env}