Program: avoid staying in program mode after a failed Program command

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

2 files changed, 8 insertions, 21 deletions

diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 22ac6e90c1..4c12b4e7ba 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1620,12 +1620,15 @@ let interp c = match c with
   (* Extensions *)
   | VernacExtend (opn,args) -> Vernacinterp.call (opn,args)
 
-let interp c = 
+let interp c =
   let mode = Flags.is_program_mode () in
-    (try Obligations.set_program_mode !program_flag
-     with e -> program_flag := false; raise e);
+  let isprogcmd = !Flags.program_cmd in
+  Flags.program_cmd := false;
+  Obligations.set_program_mode isprogcmd;
+  try
     interp c; check_locality ();
-    program_flag := false;
     Flags.program_mode := mode
-  (* with_program_flag (fun () -> interp c ; check_locality ()) *)
+  with e ->
+    Flags.program_mode := mode;
+    raise e
 
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index c8729bfa97..95384c1c94 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -495,19 +495,3 @@ let use_module_locality () =
 
 let enforce_module_locality local =
   make_module_locality (enforce_locality_full local)
-
-(**********************************************************************)
-
-(**********************************************************************)
-(* Managing the Program extension. *)
-
-let program_flag = ref false
-let with_program_flag m = 
-  if Flags.is_program_mode () then
-    (program_flag := false; m ())
-  else if !program_flag then 
-    (Flags.program_mode := true; 
-     m ();
-     Flags.program_mode := false;
-     program_flag := false)
-