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, 8 deletions

diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index fa4a0d0ff..24e2b5d8d 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -35,10 +35,7 @@ let print_memory_stat () =
 let _ = at_exit print_memory_stat
 
 let engagement = ref None
-let set_engagement c =
-  if !engagement <> None then error
-    "Options strongly-constructive/strongly-classical occur more than once";
-  engagement := Some c
+let set_engagement c = engagement := Some c
 let engage () =
   match !engagement with Some c -> Global.set_engagement c | None -> ()
   
@@ -154,10 +151,8 @@ let parse_args is_ide =
   let rec parse = function
     | [] -> ()
 
-    | "-strongly-constructive" :: rem -> 
-        set_engagement Environ.StronglyConstructive; parse rem
-    | "-strongly-classical" :: rem -> 
-        set_engagement Environ.StronglyClassical; parse rem
+    | "-impredicative-set" :: rem -> 
+        set_engagement Environ.ImpredicativeSet; parse rem
 
     | ("-I"|"-include") :: d :: rem -> set_default_include d; parse rem
     | ("-I"|"-include") :: []       -> usage ()