From a2bf0916e0b96d404da91eae273a62469635510d Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Wed, 8 Jan 2014 19:28:49 +0100
Subject: Fix base_include: Toplevel-->Coqloop, Constrintern.intern_constr
 without evd

---
 dev/base_include | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

(limited to 'dev/base_include')

diff --git a/dev/base_include b/dev/base_include
index 94146102be..26ebad9662 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -160,7 +160,7 @@ open Himsg
 open Metasyntax
 open Mltop
 open Record
-open Toplevel
+open Coqloop
 open Vernacentries
 open Vernacinterp
 open Vernac
@@ -178,8 +178,7 @@ let parse_vernac = Pcoq.parse_string Pcoq.Vernac_.vernac;;
 (* build a term of type glob_constr without type-checking or resolution of 
    implicit syntax *)
 
-let e s =
-  Constrintern.intern_constr Evd.empty (Global.env()) (parse_constr s);;
+let e s = Constrintern.intern_constr (Global.env()) (parse_constr s);;
 
 (* build a term of type constr with type-checking and resolution of 
    implicit syntax *)
@@ -211,7 +210,7 @@ let _ = Constrextern.in_debugger := false
 let _ = Constrextern.set_extern_reference
   (fun loc _ r -> Libnames.Qualid (loc,Nametab.shortest_qualid_of_global Idset.empty r));;
 
-open Toplevel
+open Coqloop
 let go = loop
 
 let _ =
-- 
cgit v1.2.3