aboutsummaryrefslogtreecommitdiff
path: root/API
AgeCommit message (Expand)Author
2017-06-16Fix bugs and add an option for cumulativityAmin Timany
2017-06-16Squashed commit of the following:Amin Timany
2017-06-16Using UInfoInd for universes in inductive typesAmin Timany
2017-06-16Extend definition of inductives to include subtyping infoAmin Timany
2017-06-15Merge PR#719: Constrexpr.Numeral without bigintMaxime Dénès
2017-06-15Merge PR#769: [lib] Remove obsolete state-management function add_frozen_stateMaxime Dénès
2017-06-14Merge PR#763: [proof] Deprecate redundant wrappers.Maxime Dénès
2017-06-14Merge PR#513: A fix to #5414 (ident bound by ltac names now known for "match").Maxime Dénès
2017-06-14Merge PR#622: Change the default flag value for Refine.refineMaxime Dénès
2017-06-14API: exports Mltop.module_is_known to both API.mli and grammar_API.mliPierre Letouzey
2017-06-14G_prim: the bigint entry keeps numbers in raw stringsPierre Letouzey
2017-06-14Constrexpr.Numeral stays uninterpreted (string+sign instead of BigInt.t)Pierre Letouzey
2017-06-13Dualize the unsafe flag of refine into typecheck and make it mandatory.Pierre-Marie Pédrot
2017-06-12[lib] Remove obsolete state-management function add_frozen_stateEmilio Jesus Gallego Arias
2017-06-11[proof] Deprecate redundant wrappers.Emilio Jesus Gallego Arias
2017-06-10Remove (useless) aliases from the API.Matej Košík
2017-06-09A fix to #5414 (ident bound by ltac names now known for "match").Hugo Herbelin
2017-06-07Put "ssreflect" behind "API".Matej Košík
2017-06-07Put all plugins behind an "API".Matej Kosik
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 14:36:29 +0000