diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:42:51 +0100 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:42:51 +0100 |
commit | 7cfc4e5146be5666419451bdd516f1f3f264d24a (patch) | |
tree | e4197645da03dc3c7cc84e434cc31d0a0cca7056 /dev/include | |
parent | 420f78b2caeaaddc6fe484565b2d0e49c66888e5 (diff) |
Imported Upstream version 8.5~beta1+dfsg
Diffstat (limited to 'dev/include')
-rw-r--r-- | dev/include | 36 |
1 files changed, 32 insertions, 4 deletions
diff --git a/dev/include b/dev/include index 69ac3c41..b2eb280d 100644 --- a/dev/include +++ b/dev/include @@ -10,8 +10,9 @@ Alternatively, you can avoid typing #use "include" after each Drop by adding the following lines in your $HOME/.ocamlinit : + #directory "+compiler-libs";; if Filename.basename Sys.argv.(0) = "coqtop.byte" - then ignore (Toploop.use_silently Format.std_formatter "include") + then ignore (Toploop.use_silently Format.std_formatter "dev/include") *) (* For OCaml 3.10.x: @@ -28,25 +29,50 @@ #install_printer (* pattern *) pppattern;; #install_printer (* glob_constr *) ppglob_constr;; - +#install_printer (* open constr *) ppopenconstr;; #install_printer (* constr *) ppconstr;; #install_printer (* constr_substituted *) ppsconstr;; +#install_printer (* constraints *) ppconstraints;; +#install_printer (* univ constraints *) ppuniverseconstraints;; #install_printer (* universe *) ppuni;; +#install_printer (* universes *) ppuniverse;; #install_printer (* universes *) ppuniverses;; +#install_printer (* univ level *) ppuni_level;; +#install_printer (* univ context *) ppuniverse_context;; +#install_printer (* univ context future *) ppuniverse_context_future;; +#install_printer (* univ context set *) ppuniverse_context_set;; +#install_printer (* univ set *) ppuniverse_set;; +#install_printer (* univ instance *) ppuniverse_instance;; +#install_printer (* univ subst *) ppuniverse_subst;; +#install_printer (* univ full subst *) ppuniverse_level_subst;; +#install_printer (* univ opt subst *) ppuniverse_opt_subst;; +#install_printer (* evar univ ctx *) ppevar_universe_context;; +#install_printer (* constraints_map *) ppconstraints_map;; +#install_printer (* inductive *) ppind;; +#install_printer (* 'a scheme_kind *) ppscheme;; #install_printer (* type_judgement *) pptype;; #install_printer (* judgement *) ppj;; +#install_printer (* id set *) ppidset;; +#install_printer (* int set *) ppintset;; + +#install_printer (* Reductionops stcak of unfolded constants *) pp_cst_stack_t;; +#install_printer (* Reductionops machine stack *) pp_stack_t;; -#install_printer (* hint_db *) print_hint_db;; +(*#install_printer (* hint_db *) print_hint_db;;*) (*#install_printer (* hints_path *) pphintspath;;*) #install_printer (* goal *) ppgoal;; (*#install_printer (* sigma goal *) ppsigmagoal;;*) (*#install_printer (* proof *) pproof;;*) #install_printer (* Goal.goal *) ppgoalgoal;; +#install_printer (* proofview *) ppproofview;; #install_printer (* metaset.t *) ppmetas;; +#install_printer (* evar *) ppevar;; #install_printer (* evar_map *) ppevm;; -#install_printer (* ExistentialSet.t *) ppexistentialset;; +#install_printer (* Evar.Set.t *) ppexistentialset;; #install_printer (* clenv *) ppclenv;; #install_printer (* env *) ppenv;; +#install_printer (* Hint_db.t *) pphintdb;; +#install_printer (* named_context_val *) ppnamedcontextval;; #install_printer (* tactic *) pptac;; #install_printer (* object *) ppobj;; @@ -54,3 +80,5 @@ #install_printer (* generic_argument *) pp_generic_argument;; #install_printer (* fconstr *) ppfconstr;; + +#install_printer (* Future.computation *) ppfuture;; |