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

5 files changed, 8 insertions, 21 deletions

diff --git a/kernel/environ.ml b/kernel/environ.ml
index 7b1eff341..4a2c37a4a 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -23,7 +23,7 @@ type compilation_unit_name = dir_path * checksum
 
 type global = Constant | Inductive
 
-type engagement = StronglyConstructive | StronglyClassical
+type engagement = ImpredicativeSet
 
 type globals = {
   env_constants : constant_body KNmap.t;
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 4a18224a0..540fd02d3 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -36,7 +36,7 @@ val universes     : env -> Univ.universes
 val rel_context   : env -> rel_context
 val named_context : env -> named_context
 
-type engagement = StronglyConstructive | StronglyClassical
+type engagement = ImpredicativeSet
 
 val engagement    : env -> engagement option
 
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index ba7389915..c5b298955 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -151,8 +151,8 @@ let small_unit constrsinfos =
 let enforce_type_constructor env arsort smax cst =
   match smax, arsort with
     | Type uc, Type ua -> enforce_geq ua uc cst
-    | Type uc, Prop Pos when engagement env <> Some StronglyConstructive ->
-        error "Large inductive types must be in Type, unless option -strongly-constructive is set"
+    | Type uc, Prop Pos when engagement env <> Some ImpredicativeSet ->
+        error "Large non-propositional inductive types must be in Type"
     | _,_ -> cst
 
 let type_one_constructor env_ar_par params arsort c =
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 5dc988328..d007af08e 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}
 
 
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 96e3cabd4..46ee8d97e 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -198,7 +198,7 @@ let sort_of_product env domsort rangsort =
     | (Prop _,  Prop Pos) -> rangsort
     (* Product rule (Type,Set,?) *)
     | (Type u1, Prop Pos) ->
-        if engagement env = Some StronglyConstructive then
+        if engagement env = Some ImpredicativeSet then
           (* Rule is (Type,Set,Set) in the Set-impredicative calculus *)
           rangsort
         else