Merge from Lionel Elie Mamane's private branch:

 - Makefile: Option (environment variable NO_RECOMPILE_LIB) to not
   recompile the whole standard library just because the coq binaries
   got rebuilt.

 - Infrastructure to change the object pretty-printers at runtime.

 - Use that infrastructure to make coqtop-protocol with Pcoq trees and
   Pcoq-protocol with pretty-printed terms possible in coq-interface.

 - Make "Back(track)" into closed sections, modules and module types
   "Just Work™".

 - Modernise/generalise Pcoq protocol a bit, make some of its warts
   optional.

 - Implement "Show." in Pcoq mode.

 - Add Rpow_def.vo to REALSBASEVO so that its dependencies are
   computed (and used).

 - "make revision" now handles GNU Arch / tla in addition to svn.



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

1 files changed, 13 insertions, 12 deletions

diff --git a/contrib/interface/parse.ml b/contrib/interface/parse.ml
index 0278a16cd5..b551b143c2 100644
--- a/contrib/interface/parse.ml
+++ b/contrib/interface/parse.ml
@@ -21,18 +21,19 @@ type parsed_tree =
   | P_i of ct_INT;;
 
 let print_parse_results n msg =
-  print_string "message\nparsed\n";
-  print_int n;
-  print_string "\n";
-  (match msg with
-  | P_cl x -> fCOMMAND_LIST x
-  | P_c x -> fCOMMAND x
-  | P_t x -> fTACTIC_COM x
-  | P_f x -> fFORMULA x
-  | P_id x -> fID x
-  | P_s x -> fSTRING x
-  | P_i x -> fINT x);
-  print_string "e\nblabla\n";
+  Pp.msg
+  ( str "message\nparsed\n" ++
+    int n ++
+    str "\n" ++
+    (match msg with
+     | P_cl x -> fCOMMAND_LIST x
+     | P_c x -> fCOMMAND x
+     | P_t x -> fTACTIC_COM x
+     | P_f x -> fFORMULA x
+     | P_id x -> fID x
+     | P_s x -> fSTRING x
+     | P_i x -> fINT x) ++
+    str "e\nblabla\n");
   flush stdout;;
 
 let ctf_SyntaxErrorMessage reqid pps =