Options -strongly-constructive et -strongly-classical

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

1 files changed, 14 insertions, 0 deletions

diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 85a289ff3..a7ff15cee 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -34,6 +34,14 @@ 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 engage () =
+  match !engagement with Some c -> Global.set_engagement c | None -> ()
+  
 let set_batch_mode () = batch_mode := true
 
 let remove_top_ml () = Mltop.remove ()
@@ -142,6 +150,11 @@ 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
+
     | ("-I"|"-include") :: d :: rem -> set_default_include d; parse rem
     | ("-I"|"-include") :: []       -> usage ()
 
@@ -265,6 +278,7 @@ let init is_ide =
       if_verbose print_header ();
       init_load_path ();
       inputstate ();
+      engage ();
       init_library_roots ();
       load_vernac_obj ();
       require ();