diff options
Diffstat (limited to 'dev/base_include')
| -rw-r--r-- | dev/base_include | 13 |
1 files changed, 6 insertions, 7 deletions
diff --git a/dev/base_include b/dev/base_include index 1fb80dc0..6f54ecb2 100644 --- a/dev/base_include +++ b/dev/base_include @@ -15,7 +15,6 @@ #directory "tactics";; #directory "printing";; #directory "grammar";; -#directory "intf";; #directory "stm";; #directory "vernac";; @@ -109,8 +108,6 @@ open Inductiveops open Locusops open Find_subterm open Unification -open Miscops -open Miscops open Nativenorm open Typeclasses open Typeclasses_errors @@ -190,7 +187,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 +202,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 +229,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 |