1 files changed, 8 insertions, 12 deletions
diff --git a/dev/base_include b/dev/base_include
index 1fb80dc074..48feeec147 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -8,6 +8,7 @@
 #directory "toplevel";;
 #directory "library";;
 #directory "kernel";;
+#directory "gramlib";;
 #directory "engine";;
 #directory "pretyping";;
 #directory "lib";;
@@ -15,12 +16,9 @@
 #directory "tactics";;
 #directory "printing";;
 #directory "grammar";;
-#directory "intf";;
 #directory "stm";;
 #directory "vernac";;
 
-#directory "+camlp5";; (* Gramext is found in top_printers.ml *)
-
 #use "top_printers.ml";;
 #use "vm_printers.ml";;
 
@@ -100,7 +98,6 @@ open Evarutil
 open Evarsolve
 open Tacred
 open Evd
-open Universes
 open Termops
 open Namegen
 open Indrec
@@ -109,8 +106,6 @@ open Inductiveops
 open Locusops
 open Find_subterm
 open Unification
-open Miscops
-open Miscops
 open Nativenorm
 open Typeclasses
 open Typeclasses_errors
@@ -139,7 +134,6 @@ open Pfedit
 open Proof
 open Proof_using
 open Proof_global
-open Proof_type
 open Redexpr
 open Refiner
 open Tacmach
@@ -180,7 +174,7 @@ open Mltop
 open Record
 open Coqloop
 open Vernacentries
-open Vernacinterp
+open Vernacextend
 open Vernac
 
 (* Various utilities *)
@@ -190,7 +184,7 @@ 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_control;;
+let parse_vernac = Pcoq.parse_string Pvernac.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 
@@ -205,7 +199,9 @@ let e s =
    implicit syntax *)
 
 let constr_of_string s = 
-  Constrintern.interp_constr (Global.env()) Evd.empty (parse_constr s);;
+  let env = Global.env () in
+  let sigma = Evd.from_env env in
+  Constrintern.interp_constr env sigma (parse_constr s);;
 
 (* get the body of a constant *)
 
@@ -230,9 +226,9 @@ let pf_e gl s =
 let _ = Flags.in_debugger := false
 let _ = Flags.in_toplevel := true
 let _ = Constrextern.set_extern_reference
-  (fun ?loc _ r -> CAst.make ?loc @@ Libnames.Qualid (Nametab.shortest_qualid_of_global Id.Set.empty r));;
+  (fun ?loc _ r -> Nametab.shortest_qualid_of_global ?loc Id.Set.empty r);;
 
-let go () = Coqloop.loop ~time:false ~state:Option.(get !Coqloop.drop_last_doc)
+let go () = Coqloop.(loop ~opts:Option.(get !drop_args) ~state:Option.(get !drop_last_doc))
 
 let _ =
  print_string