diff options
Diffstat (limited to 'dev/base_include')
| -rw-r--r-- | dev/base_include | 63 |
1 files changed, 45 insertions, 18 deletions
diff --git a/dev/base_include b/dev/base_include index 9a788b7b..de63c557 100644 --- a/dev/base_include +++ b/dev/base_include @@ -12,7 +12,10 @@ #directory "lib";; #directory "proofs";; #directory "tactics";; -#directory "translate";; +#directory "printing";; +#directory "grammar";; +#directory "intf";; +#directory "stm";; #directory "+camlp4";; (* lazy solution: add both of camlp4/5 so that *) #directory "+camlp5";; (* Gramext is found in top_printers.ml *) @@ -31,14 +34,17 @@ #install_printer (* qualid *) ppqualid;; #install_printer (* kernel_name *) ppkn;; #install_printer (* constant *) ppcon;; +#install_printer (* projection *) ppproj;; #install_printer (* cl_index *) ppclindex;; -#install_printer (* constr *) print_pure_constr;; +#install_printer (* recarg Rtree.t *) ppwf_paths;; +#install_printer (* constr *) print_pure_constr;; #install_printer (* patch *) ppripos;; #install_printer (* values *) ppvalues;; #install_printer (* Idpred.t *) pp_idpred;; #install_printer (* Cpred.t *) pp_cpred;; #install_printer ppzipper;; #install_printer ppstack;; +#install_printer (* Reductionops.Stack.t *) pp_stack_t;; #install_printer ppatom;; #install_printer ppwhd;; #install_printer ppvblock;; @@ -50,6 +56,8 @@ open Names open Term +open Vars +open Context open Typeops open Term_typing open Univ @@ -63,38 +71,48 @@ open Declare open Declaremods open Impargs open Libnames +open Globnames open Nametab open Library open Cases open Pattern +open Patternops open Cbv open Classops +open Arguments_renaming open Pretyping -open Pretyping.Default -open Pretyping.Default.Cases open Cbv open Classops open Clenv open Clenvtac open Glob_term +open Glob_ops open Coercion -open Coercion.Default open Recordops open Detyping open Reductionops open Evarconv open Retyping open Evarutil +open Evarsolve open Tacred open Evd +open Universes open Termops open Namegen open Indrec open Typing open Inductiveops +open Locusops +open Find_subterm open Unification -open Matching +open Miscops +open Miscops +open Nativenorm +open Typeclasses +open Typeclasses_errors +open Vnorm open Constrextern open Constrintern @@ -105,19 +123,28 @@ open Notation open Ppextend open Reserve open Syntax_def +open Constrexpr +open Constrexpr_ops open Topconstr +open Notation_term +open Notation_ops open Prettyp open Search open Evar_refiner +open Goal open Logic open Pfedit +open Proof +open Proof_using +open Proof_global open Proof_type open Redexpr open Refiner open Tacmach -open Decl_proof_instr open Tactic_debug + +open Decl_proof_instr open Decl_mode open Auto @@ -129,11 +156,11 @@ open Equality open Evar_tactics open Extraargs open Extratactics -open Hiddentac open Hipattern open Inv open Leminv -open Refine +open Tacsubst +open Tacintern open Tacinterp open Tacticals open Tactics @@ -145,7 +172,6 @@ open Command open Indschemes open Ind_tables open Auto_ind_decl -open Lemmas open Coqinit open Coqtop open Discharge @@ -153,7 +179,7 @@ open Himsg open Metasyntax open Mltop open Record -open Toplevel +open Coqloop open Vernacentries open Vernacinterp open Vernac @@ -171,22 +197,22 @@ 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 *) let constr_of_string s = - Constrintern.interp_constr Evd.empty (Global.env()) (parse_constr s);; + Constrintern.interp_constr (Global.env()) Evd.empty (parse_constr s);; (* get the body of a constant *) open Declarations;; +open Declareops;; let constbody_of_string s = let b = Global.lookup_constant (Nametab.locate_constant (qualid_of_string s)) in - Option.get (body_of_constant b);; + Option.get (Declareops.body_of_constant Opaqueproof.empty_opaquetab b);; (* Get the current goal *) (* @@ -196,14 +222,15 @@ 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);; + Constrintern.interp_constr (pf_env gl) (project gl) (parse_constr s);; (* Set usual printing since the global env is available from the tracer *) -let _ = Constrextern.in_debugger := false +let _ = Flags.in_debugger := false +let _ = Flags.in_toplevel := true 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 _ = |