aboutsummaryrefslogtreecommitdiff
path: root/API/API.mli
AgeCommit message (Expand)Author
2017-06-21[vernac] Remove stale bool parameter from `VernacStartTheoremProof`Emilio Jesus Gallego Arias
2017-06-20Merge PR#774: [ide] Add route_id parameter to query call.Maxime Dénès
2017-06-20Merge PR#803: Clean ssrMaxime Dénès
2017-06-19Merge PR#613: Cumulativity for inductive typesMaxime Dénès
2017-06-19Merge PR#784: API additions for coq-dpdgraphMaxime Dénès
2017-06-18[ide] Add route_id parameter to query call.Emilio Jesus Gallego Arias
2017-06-16Removing Proof_type from the API.Pierre-Marie Pédrot
2017-06-16A short cleanupAmin Timany
2017-06-16Clean up universes of constants and inductivesAmin Timany
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-14API additions for coq-dpdgraphGaëtan Gilbert
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 17:41:29 +0000