summaryrefslogtreecommitdiff
path: root/dev/base_include
diff options
context:
space:
mode:
Diffstat (limited to 'dev/base_include')
-rw-r--r--dev/base_include19
1 files changed, 10 insertions, 9 deletions
diff --git a/dev/base_include b/dev/base_include
index 05e87da1..d1125965 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -24,7 +24,6 @@
#install_printer (* identifier *) ppidset;;
#install_printer (* Intset.t *) ppintset;;
#install_printer (* label *) pplab;;
-(*#install_printer (* mod_self_id *) ppmsid;;*)
#install_printer (* mod_bound_id *) ppmbid;;
#install_printer (* dir_path *) ppdir;;
#install_printer (* module_path *) ppmp;;
@@ -38,7 +37,6 @@
#install_printer (* values *) ppvalues;;
#install_printer (* Idpred.t *) pp_idpred;;
#install_printer (* Cpred.t *) pp_cpred;;
-#install_printer (* transparent_state *) pp_transparent_state;;
#install_printer ppzipper;;
#install_printer ppstack;;
#install_printer ppatom;;
@@ -78,7 +76,8 @@ open Pretyping.Default.Cases
open Cbv
open Classops
open Clenv
-open Rawterm
+open Clenvtac
+open Glob_term
open Coercion
open Coercion.Default
open Recordops
@@ -110,11 +109,9 @@ open Topconstr
open Prettyp
open Search
-open Clenvtac
open Evar_refiner
open Logic
open Pfedit
-open Proof_trees
open Proof_type
open Redexpr
open Refiner
@@ -172,7 +169,7 @@ 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;;
-(* build a term of type rawconstr without type-checking or resolution of
+(* build a term of type glob_constr without type-checking or resolution of
implicit syntax *)
let e s =
@@ -190,18 +187,22 @@ open Declarations;;
let constbody_of_string s =
let b = Global.lookup_constant (Nametab.locate_constant (qualid_of_string s)) in
- Option.get b.const_body;;
+ Option.get (body_of_constant b);;
(* Get the current goal *)
-
+(*
let getgoal x = top_goal_of_pftreestate (Pfedit.get_pftreestate x);;
let get_nth_goal n = nth_goal_of_pftreestate n (Pfedit.get_pftreestate ());;
let current_goal () = get_nth_goal 1;;
-
+*)
let pf_e gl s =
Constrintern.interp_constr (project gl) (pf_env gl) (parse_constr s);;
open Toplevel
let go = loop
+let _ =
+ print_string
+ ("\n\tOcaml toplevel with Coq printers and utilities (use go();; to exit)\n\n");
+ flush_all()