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, 1 insertions, 0 deletions

diff --git a/contrib/interface/translate.mli b/contrib/interface/translate.mli
index 65d8331b2d..34841fc4b6 100644
--- a/contrib/interface/translate.mli
+++ b/contrib/interface/translate.mli
@@ -5,6 +5,7 @@ open Environ;;
 open Term;;
 
 val translate_goal : goal -> ct_RULE;;
+val translate_goals : goal list -> ct_RULE_LIST;;
 (* The boolean argument indicates whether names from the environment should *)
 (*  be avoided (same interpretation as for prterm_env and ast_of_constr)    *)
 val translate_constr : bool -> env -> constr -> ct_FORMULA;;