1 files changed, 12 insertions, 15 deletions
diff --git a/dev/base_include b/dev/base_include
index b09b6df2..1fb80dc0 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -17,9 +17,8 @@
 #directory "grammar";;
 #directory "intf";;
 #directory "stm";;
-#directory "ltac";;
+#directory "vernac";;
 
-#directory "+camlp4";; (* lazy solution: add both of camlp4/5 so that *)
 #directory "+camlp5";; (* Gramext is found in top_printers.ml *)
 
 #use "top_printers.ml";;
@@ -52,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 *)
 
@@ -128,7 +127,6 @@ open Reserve
 open Syntax_def
 open Constrexpr
 open Constrexpr_ops
-open Topconstr
 open Notation_term
 open Notation_ops
 open Prettyp
@@ -147,9 +145,6 @@ open Refiner
 open Tacmach
 open Tactic_debug
 
-open Decl_proof_instr
-open Decl_mode
-
 open Hints
 open Auto
 open Autorewrite
@@ -172,7 +167,7 @@ open Eqschemes
 
 open ExplainErr
 open Class
-open Command
+open ComDefinition
 open Indschemes
 open Ind_tables
 open Auto_ind_decl
@@ -195,13 +190,16 @@ let qid = Libnames.qualid_of_string;;
 (* parsing of terms *)
 
 let parse_constr = Pcoq.parse_string Pcoq.Constr.constr;;
-let parse_tac    = Pcoq.parse_string Pcoq.Tactic.tactic;;
-let parse_vernac = Pcoq.parse_string Pcoq.Vernac_.vernac;;
+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 *)
 
-let e s = Constrintern.intern_constr (Global.env()) (parse_constr s);;
+let e s =
+  let env = Global.env () in
+  let sigma = Evd.from_env env in
+  Constrintern.intern_constr env sigma (parse_constr s);;
 
 (* build a term of type constr with type-checking and resolution of 
    implicit syntax *)
@@ -216,7 +214,7 @@ open Declareops;;
 
 let constbody_of_string s =
   let b = Global.lookup_constant (Nametab.locate_constant (qualid_of_string s)) in
-  Option.get (Declareops.body_of_constant Opaqueproof.empty_opaquetab b);;
+  Option.get (Global.body_of_constant_body b);;
 
 (* Get the current goal *)
 (*
@@ -232,10 +230,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 -> CAst.make ?loc @@ Libnames.Qualid (Nametab.shortest_qualid_of_global Id.Set.empty r));;
 
-open Coqloop
-let go = loop
+let go () = Coqloop.loop ~time:false ~state:Option.(get !Coqloop.drop_last_doc)
 
 let _ =
  print_string