1 files changed, 6 insertions, 11 deletions
diff --git a/dev/base_include b/dev/base_include
index 79ecd73e0d..350ccaa109 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -18,12 +18,9 @@
 #directory "intf";;
 #directory "stm";;
 #directory "vernac";;
-#directory "../API";;
 
-#directory "+camlp4";; (* lazy solution: add both of camlp4/5 so that *)
 #directory "+camlp5";; (* Gramext is found in top_printers.ml *)
 
-#load "API.cma";;
 #use "top_printers.ml";;
 #use "vm_printers.ml";;
 
@@ -54,7 +51,7 @@
 #install_printer ppvblock;;
 #install_printer  (* bigint *) ppbigint;;
 #install_printer  (* loc *) pploc;;
-#install_printer  (* substitution *) prsubst;;
+#install_printer  (* substitution *) ppsubst;;
 
 (* Open main files *)
 
@@ -130,7 +127,6 @@ open Reserve
 open Syntax_def
 open Constrexpr
 open Constrexpr_ops
-open Topconstr
 open Notation_term
 open Notation_ops
 open Prettyp
@@ -171,7 +167,7 @@ open Eqschemes
 
 open ExplainErr
 open Class
-open Command
+open ComDefinition
 open Indschemes
 open Ind_tables
 open Auto_ind_decl
@@ -194,8 +190,8 @@ let qid = Libnames.qualid_of_string;;
 (* parsing of terms *)
 
 let parse_constr = Pcoq.parse_string Pcoq.Constr.constr;;
-let parse_vernac = Pcoq.parse_string Pcoq.Vernac_.vernac;;
-let parse_tac    = API.Pcoq.parse_string Ltac_plugin.Pltac.tactic;;
+let parse_vernac = Pcoq.parse_string Pcoq.Vernac_.vernac_control;;
+let parse_tac    = Pcoq.parse_string Ltac_plugin.Pltac.tactic;;
 
 (* build a term of type glob_constr without type-checking or resolution of 
    implicit syntax *)
@@ -231,10 +227,9 @@ let pf_e gl s =
 let _ = Flags.in_debugger := false
 let _ = Flags.in_toplevel := true
 let _ = Constrextern.set_extern_reference
-  (fun ?loc _ r -> Libnames.Qualid (loc,Nametab.shortest_qualid_of_global Idset.empty r));;
+  (fun ?loc _ r -> Libnames.Qualid (loc,Nametab.shortest_qualid_of_global Id.Set.empty r));;
 
-open Coqloop
-let go = loop
+let go () = Coqloop.loop ~time:false ~state:Option.(get !Coqtop.drop_last_doc)
 
 let _ =
  print_string