From a10419ad28f22e1d197bf51181b792c050e5f53e Mon Sep 17 00:00:00 2001
From: msozeau
Date: Wed, 27 Feb 2013 16:28:33 +0000
Subject: Update debug code according to reorganization into modules.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16254 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 dev/base_include          | 2 +-
 dev/db_printers.ml        | 2 +-
 toplevel/vernacentries.ml | 5 +++--
 3 files changed, 5 insertions(+), 4 deletions(-)

diff --git a/dev/base_include b/dev/base_include
index 6b10dc5992..c75413a386 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -196,7 +196,7 @@ open Declareops;;
 
 let constbody_of_string s =
   let b = Global.lookup_constant (Nametab.locate_constant (qualid_of_string s)) in
-  Option.get (body_of_constant b);;
+  Option.get (Declareops.body_of_constant b);;
 
 (* Get the current goal *)
 (*
diff --git a/dev/db_printers.ml b/dev/db_printers.ml
index 95e94c6d86..8e99c9dc72 100644
--- a/dev/db_printers.ml
+++ b/dev/db_printers.ml
@@ -11,6 +11,6 @@ open Names
 let pp s = pp (hov 0 s)
 
 let prid id = Format.print_string (Id.to_string id)
-let prsp sp = Format.print_string (string_of_path sp)
+let prsp sp = Format.print_string (DirPath.to_string sp)
 
 
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 0ef590cdf5..e735dde0dd 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1170,7 +1170,7 @@ let _ =
     { optsync  = true;
       optdepr  = false;
       optname  = "use of the program extension";
-      optkey   = ["Program"];
+      optkey   = ["Program";"Mode"];
       optread  = (fun () -> !Flags.program_mode);
       optwrite = (fun b -> Flags.program_mode:=b) }
 
@@ -1796,7 +1796,8 @@ let interp c =
   Obligations.set_program_mode isprogcmd;
   try
     interp c; Locality.check_locality ();
-    Flags.program_mode := mode;
+    if not (not mode && !Flags.program_mode && not isprogcmd) then
+      Flags.program_mode := mode;
     true
   with e ->
     let e = Errors.push e in
-- 
cgit v1.2.3