aboutsummaryrefslogtreecommitdiff
path: root/theories/Init
AgeCommit message (Expand)Author
2019-10-29Use a less kludgy way of solving #9114Jason Gross
2019-10-29Fix #9114, assert_succeeds (exact I) solves goalJason Gross
2019-10-29`assert_succeeds`&`assert_fails`: multisuccess fixJason Gross
2019-09-16Fix #10757: Program Fixpoint uses "exists" for telescopesGaëtan Gilbert
2019-09-09Merge PR #9379: Vectors: lemmas about uncons and splitAtHugo Herbelin
2019-09-01edits per reviewYishuai Li
2019-09-01Vectors: lemmas about uncons and splitAtYishuai Li
2019-08-26Make kernel parametric on the lowest universe and fix #9294Matthieu Sozeau
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-05-25Modifying theories to preferably use the "[= ]" syntax, and,Hugo Herbelin
2019-05-23Fixing typos - Part 3JPR
2019-04-05Merge PR #8764: Add parsing of decimal constants (e.g., 1.02e+01)Emilio Jesus Gallego Arias
2019-04-03Merge PR #8638: Remove -compat 8.7Théo Zimmermann
2019-04-02Remove -compat 8.7Jason Gross
2019-04-02Add parsing of decimal constants (e.g., 1.02e+01)Pierre Roux
2019-03-26Declare initial hint databases in preludeMaxime Dénès
2019-03-14Add StrictProp.v with basic SProp related definitionsGaëtan Gilbert
2019-02-04Merge PR #9386: Pass some files to strict focusing mode.Pierre-Marie Pédrot
2019-01-31Fix off-by-one error in nat syntax warningsJason Gross
2019-01-25[Numeral notations] Use Coqlib registered constantsVincent Laporte
2019-01-23Pass some files to strict focusing mode.Gaëtan Gilbert
2018-12-19Put #[universes(template)] on all auto template spots in stdlibGaëtan Gilbert
2018-11-28Byte.v: use right-associative tuples in bitsJason Gross
2018-11-28Speed up ByteJason Gross
2018-11-28Add `String Notation` vernacular like `Numeral Notation`Jason Gross
2018-11-14Deprecate hint declaration/removal with no specified databaseMaxime Dénès
2018-10-10[coqlib] Rebindable Coqlib namespace.Emilio Jesus Gallego Arias
2018-10-02Update compat notations to be compat 8.7Jason Gross
2018-09-25Adding lemmas about dependent equality.Hugo Herbelin
2018-09-25Mini refreshing layout Datatypes.v.Hugo Herbelin
2018-09-25Adding f_equal_dep in Logic.v.Hugo Herbelin
2018-09-10Adapting standard library to the introduction of "Declare Scope".Hugo Herbelin
2018-08-31Decimal: scope name changed dec_(u)int_scopePierre Letouzey
2018-08-31Numeral Notation for natPierre Letouzey
2018-08-31Numeral Notation: allow parsing from/to Decimal.int or Decimal.uintPierre Letouzey
2018-08-31Prelude : update the comment about ML plugins loaded by InitPierre Letouzey
2018-07-10Fix typo in Init.Logic.whitequark
2018-07-02hints: add Hint Variables/Constants Opaque/Transparent commandsMatthieu Sozeau
2018-03-09Merge PR #6820: Tacticals assert_fails and assert_succeedsMaxime Dénès
2018-03-08Merge PR #6522: Fix core hint database issue #6521Maxime Dénès
2018-03-08Merge PR #6743: Add notation {x & P} for sigTMaxime Dénès
2018-03-05Merge PR #6855: Update headers following #6543.Maxime Dénès
2018-03-02Remove the deprecation for some 8.2-8.5 compatibility aliases.Théo Zimmermann
2018-02-28Uniform spacing layout in Tactics.v.Hugo Herbelin
2018-02-28Added tacticals assert_succeeds/assert_fails (courtesy of Jason Gross).Hugo Herbelin
2018-02-27Update headers following #6543.Théo Zimmermann
2018-02-24Merge PR #6599: Decimals in preludeMaxime Dénès
2018-02-20Decimal: proofs that conversions from/to nat,N,Z are bijectionsPierre Letouzey
2018-02-20Decimal: simple representation of base-10 numbersPierre Letouzey
2018-02-20Trying a hack to support {'pat|P} without breaking compatibility.Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-25 06:00:57 +0000