diff options
| author | Pierre Letouzey | 2014-01-08 19:28:49 +0100 |
|---|---|---|
| committer | Pierre Letouzey | 2014-01-08 19:28:49 +0100 |
| commit | a2bf0916e0b96d404da91eae273a62469635510d (patch) | |
| tree | 47784ce3e495c74ed2486464c95e14c352cc05a5 /dev/base_include | |
| parent | a43fc367fb43d222a99e5f8806370103d0650c7d (diff) | |
Fix base_include: Toplevel-->Coqloop, Constrintern.intern_constr without evd
Diffstat (limited to 'dev/base_include')
| -rw-r--r-- | dev/base_include | 7 |
1 files changed, 3 insertions, 4 deletions
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 _ = |