aboutsummaryrefslogtreecommitdiff
path: root/theories/Init
AgeCommit message (Expand)Author
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
2017-06-13Merge PR#385: Equality of sigma typesMaxime Dénès
2017-06-01drop vo.itarget files and compute the corresponding the corresponding values ...Matej Kosik
2017-05-28More uniform indentation of sigma lemmasJason Gross
2017-05-28Give explicit proof terms to proj2_sig_eq etc.Jason Gross
2017-05-28Use the rew dependent notation in ex, ex2 proofsJason Gross
2017-05-28Make theorems about ex equality QedJason Gross
2017-05-28Make new proofs of equality QedJason Gross
2017-05-28Add some more comments about sigma equalitiesJason Gross
2017-05-28Remove motive argument from [rew dependent]Jason Gross
2017-05-28Use a local [rew dependent] notationJason Gross
2017-05-28Add forward-chaining versions: [eq_sig*_uncurried]Jason Gross
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-30 05:57:36 +0000