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

2 files changed, 8 insertions, 7 deletions

diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 4c24f3505..9d8bbcc00 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -44,8 +44,8 @@ type pcoq_hook = {
   abort : string -> unit;
   search : searchable -> dir_path list * bool -> unit;
   print_name : reference -> unit;
-  print_check : Environ.unsafe_judgment -> unit;
-  print_eval : (constr -> constr) -> Environ.env -> constr_expr -> 
+  print_check : Environ.env -> Environ.unsafe_judgment -> unit;
+  print_eval : Reductionops.reduction_function -> Environ.env -> Evd.evar_map -> constr_expr ->
     Environ.unsafe_judgment -> unit;
   show_goal : int option -> unit
 }
@@ -888,13 +888,13 @@ let vernac_check_may_eval redexp glopt rc =
   let j = Typeops.typing env c in
   match redexp with
     | None ->
-	if !pcoq <> None then (out_some !pcoq).print_check j
+	if !pcoq <> None then (out_some !pcoq).print_check env j
 	else msg (print_judgment env j)
     | Some r ->
 	let redfun = fst (reduction_of_red_expr (interp_redexp env evmap r)) in
 	if !pcoq <> None
-	then (out_some !pcoq).print_eval (redfun env evmap) env rc j
-	else msg (print_eval redfun env j)
+	then (out_some !pcoq).print_eval redfun env evmap rc j
+	else msg (print_eval redfun env evmap rc j)
 
   (* The same but avoiding the current goal context if any *)
 let vernac_global_check c =
diff --git a/toplevel/vernacentries.mli b/toplevel/vernacentries.mli
index e4e61c554..65464d4e2 100644
--- a/toplevel/vernacentries.mli
+++ b/toplevel/vernacentries.mli
@@ -39,8 +39,9 @@ type pcoq_hook = {
   abort : string -> unit;
   search : searchable -> dir_path list * bool -> unit;
   print_name : Libnames.reference -> unit;
-  print_check : Environ.unsafe_judgment -> unit;
-  print_eval : (constr -> constr) -> Environ.env -> constr_expr -> Environ.unsafe_judgment -> unit;
+  print_check : Environ.env -> Environ.unsafe_judgment -> unit;
+  print_eval : Reductionops.reduction_function -> Environ.env -> Evd.evar_map -> constr_expr ->
+    Environ.unsafe_judgment -> unit;
   show_goal : int option -> unit
 }