3 files changed, 21 insertions, 22 deletions
diff --git a/dev/base_include b/dev/base_include
index 3a31230f19..debc074de9 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -110,11 +110,9 @@ open Topconstr
 open Prettyp
 open Search
 
-open Clenvtac
 open Evar_refiner
 open Logic
 open Pfedit
-open Proof_trees
 open Proof_type
 open Redexpr
 open Refiner
@@ -193,12 +191,12 @@ let constbody_of_string s =
   Option.get b.const_body;;
 
 (* Get the current goal *)
-
+(*
 let getgoal x = top_goal_of_pftreestate (Pfedit.get_pftreestate x);;
 
 let get_nth_goal n = nth_goal_of_pftreestate n (Pfedit.get_pftreestate ());;
 let current_goal () = get_nth_goal 1;;
-
+*)
 let pf_e gl s = 
   Constrintern.interp_constr (project gl) (pf_env gl) (parse_constr s);;
 
diff --git a/dev/printers.mllib b/dev/printers.mllib
index e8ec10c5cd..8ada6769cc 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -12,8 +12,7 @@ Hashcons
 Dyn
 System
 Envars
-Bstack
-Edit
+Store
 Gset
 Gmap
 Fset
@@ -93,7 +92,6 @@ Coercion
 Unification
 Cases
 Pretyping
-Clenv
 
 Lexer
 Ppextend
@@ -108,12 +106,15 @@ Syntax_def
 Implicit_quantifiers
 Smartlocate
 Constrintern
-Proof_trees
 Tacexpr
 Proof_type
+Goal
 Logic
 Refiner
 Evar_refiner
+Proofview
+Proof
+Proof_global
 Pfedit
 Tactic_debug
 Decl_mode
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index b481e9f169..21a690f953 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -16,14 +16,11 @@ open Libnames
 open Nameops
 open Sign
 open Univ
-open Proof_trees
 open Environ
 open Printer
 open Tactic_printer
-open Refiner
 open Term
 open Termops
-open Clenv
 open Cerrors
 open Evd
 open Goptions
@@ -103,21 +100,24 @@ let pp_transparent_state s = pp (pr_transparent_state s)
 (* proof printers *)
 let ppmetas metas = pp(pr_metaset metas)
 let ppevm evd = pp(pr_evar_map evd)
+(* spiwack: deactivated until a replacement is found
 let ppclenv clenv = pp(pr_clenv clenv)
 let ppgoal g = pp(db_pr_goal g)
 let pppftreestate p = pp(print_pftreestate p)
+*)
 
-let pr_gls gls =
-  hov 0 (pr_evar_map (sig_sig gls) ++ fnl () ++ db_pr_goal (sig_it gls))
+(* let ppgoal g = pp(db_pr_goal g) *)
+(* let pr_gls gls = *)
+(*   hov 0 (pr_evar_defs (sig_sig gls) ++ fnl () ++ db_pr_goal (sig_it gls)) *)
 
-let pr_glls glls =
-  hov 0 (pr_evar_map (sig_sig glls) ++ fnl () ++
-         prlist_with_sep pr_fnl db_pr_goal (sig_it glls))
+(* let pr_glls glls = *)
+(*   hov 0 (pr_evar_defs (sig_sig glls) ++ fnl () ++ *)
+(*          prlist_with_sep pr_fnl db_pr_goal (sig_it glls)) *)
 
-let ppsigmagoal g = pp(pr_goal (sig_it g))
-let prgls gls = pp(pr_gls gls)
-let prglls glls = pp(pr_glls glls)
-let pproof p = pp(print_proof Evd.empty empty_named_context p)
+(* let ppsigmagoal g = pp(pr_goal (sig_it g)) *)
+(* let prgls gls = pp(pr_gls gls) *)
+(* let prglls glls = pp(pr_glls glls) *)
+(* let pproof p = pp(print_proof Evd.empty empty_named_context p) *)
 
 let ppuni u = pp(pr_uni u)
 
@@ -402,7 +402,7 @@ let _ =
   with
     e -> Pp.pp (Cerrors.explain_exn e)
 let _ =
-  extend_vernac_command_grammar "PrintConstr"
+  extend_vernac_command_grammar "PrintConstr" None
     [[GramTerminal "PrintConstr";
       GramNonTerminal
         (dummy_loc,ConstrArgType,Extend.Aentry ("constr","constr"),
@@ -419,7 +419,7 @@ let _ =
   with
     e -> Pp.pp (Cerrors.explain_exn e)
 let _ =
-  extend_vernac_command_grammar "PrintPureConstr"
+  extend_vernac_command_grammar "PrintPureConstr" None
     [[GramTerminal "PrintPureConstr";
       GramNonTerminal
         (dummy_loc,ConstrArgType,Extend.Aentry ("constr","constr"),