aboutsummaryrefslogtreecommitdiff
path: root/theories/Init
AgeCommit message (Expand)Author
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
2018-02-20Adding notations of the form "{'pat|P}", "exists2 'pat, P & Q", etc.Hugo Herbelin
2018-02-20User-level support for Gonthier-Ssreflect's "if t then pat then u else v".Hugo Herbelin
2018-02-12Add notation {x & P} for sigTTej Chajed
2018-01-03Fix core hint database issue #6521Anton Trunov
2017-12-14Add named timers to LtacProfJason Gross
2017-10-19Moving bug numbers to BZ# format in the source code.Théo Zimmermann
2017-08-29A little reorganization of notations + a fix to #5608.Hugo Herbelin
2017-07-05Fix typo in documentation for identityTej Chajed
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-06-15plugins/ltac : avoid spurious .cmxs filesPierre Letouzey
2017-06-14Prelude : no more autoload of plugins extraction and recdefPierre Letouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 11:18:13 +0000