aboutsummaryrefslogtreecommitdiff
path: root/pretyping/classops.ml
AgeCommit message (Expand)Author
2019-07-11Merge PR #10498: [api] Deprecate GlobRef constructors.Gaëtan Gilbert
2019-07-08[api] Deprecate GlobRef constructors.Emilio Jesus Gallego Arias
2019-07-08[core] [api] Support OCaml 4.08Emilio Jesus Gallego Arias
2019-07-02Improve the ambiguous paths warning to indicate which path is ambiguous with ...Kazuhiko Sakaguchi
2019-06-25Merge PR #10284: Expose set interface to option tablesPierre-Marie Pédrot
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-06-03Expose set interface to option tablesGaëtan Gilbert
2019-04-10Remove calls to global env in InductiveopsMaxime Dénès
2019-04-10Remove call to global env in pretyping.mlMaxime Dénès
2019-04-10Functionalize env in type classesMaxime Dénès
2019-04-10Move vernac-related part of coercions to vernacMaxime Dénès
2019-03-28Merge PR #9743: Relax the ambiguous path condition of coercionEnrico Tassi
2019-03-25Remove `Automatic Coercions Import` option.Maxime Dénès
2019-03-14Relax the ambiguous path condition of coercionKazuhiko Sakaguchi
2019-03-14Add relevance marks on binders.Gaëtan Gilbert
2018-12-05Fix mod_subst wrt universe polymorphismGaëtan Gilbert
2018-11-28[options] New helper for creation of boolean options plus reference.Emilio Jesus Gallego Arias
2018-11-23s/let _ =/let () =/ in some places (mostly goptions related)Gaëtan Gilbert
2018-10-26Merge PR #8687: Mini reorganization type of global constr of globalPierre-Marie Pédrot
2018-10-19Deprecating Global.type_of_global_in_context.Hugo Herbelin
2018-10-18[api] Qualify access to `Nametab`Emilio Jesus Gallego Arias
2018-10-05[kernel] Remove section paths from `KerName.t`Maxime Dénès
2018-09-19Replace trivial uses of declare_summary with summary.refsGaëtan Gilbert
2018-09-12Move maps & sets indexed by GlobRef.t into the kernelVincent Laporte
2018-09-10Remove environment passing to coercion printersGaëtan Gilbert
2018-09-07Warnings on coercions used without being ImportedMaxime Dénès
2018-07-26restore reduction of coercion to eventually expose a constructorEnrico Tassi
2018-07-26Coercions cleanup: use GlobRef.t instead of constrMaxime Dénès
2018-07-24Projections use index representationGaëtan Gilbert
2018-05-17Split off Universes functions dealing with generating new universes.Gaëtan Gilbert
2018-05-04[api] Rename `global_reference` to `GlobRef.t` to follow kernel style.Emilio Jesus Gallego Arias
2018-02-27Update headers following #6543.Théo Zimmermann
2017-12-11[proof] Embed evar_map in RefinerError exception.Emilio Jesus Gallego Arias
2017-11-06[api] Move structures deprecated in the API to the core.Emilio Jesus Gallego Arias
2017-11-06[api] Deprecate all legacy uses of Names in core.Emilio Jesus Gallego Arias
2017-09-20[flags] Flag `open Flags`Emilio Jesus Gallego Arias
2017-07-27deprecate Pp.std_ppcmds type aliasMatej Košík
2017-07-13Safer API for constr_of_global, and getting rid of unsafe_constr_of_global.Pierre-Marie Pédrot
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-06-14Deprecate options that were introduced for compatibility with 8.2.Guillaume Melquiond
2017-06-14Remove support for Coq 8.2.Guillaume Melquiond
2017-05-24[option] Remove support for non-synchronous options.Emilio Jesus Gallego Arias
2017-04-27Remove unused [open] statementsGaetan Gilbert
2017-04-21[flags] Deprecate is_silent/is_verbose in favor of single flag.Emilio Jesus Gallego Arias
2017-04-01Using delayed universe instances in EConstr.Pierre-Marie Pédrot
2017-02-14Removing compatibility layers in RetypingPierre-Marie Pédrot
2017-02-14Reductionops now return EConstrs.Pierre-Marie Pédrot
2017-02-14Tactics API using EConstr.Pierre-Marie Pédrot
2017-02-14Making judgment type generic over the type of inner constrs.Pierre-Marie Pédrot
2017-02-14Coercion API using EConstr.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 17:31:45 +0000