aboutsummaryrefslogtreecommitdiff
path: root/theories
AgeCommit message (Expand)Author
2018-07-17Remove fourier pluginMaxime Dénès
2018-07-10Fix typo in Init.Logic.whitequark
2018-07-02hints: add Hint Variables/Constants Opaque/Transparent commandsMatthieu Sozeau
2018-06-29Splitting primitive numeral parser/printer for positive, N, Z into three files.Hugo Herbelin
2018-06-10Tweak printing boxes for unicode bindersRalf Jung
2018-06-05Merge PR #7690: Fixing typos in file Berardi.vPierre-Marie Pédrot
2018-06-04Deprecate implicit tactic solving.Pierre-Marie Pédrot
2018-06-03Fixing typos in file Berardi.vHugo Herbelin
2018-04-16Protecting against a "deprecated cofix" warning.Hugo Herbelin
2018-04-13[ltac] Deprecate nameless fix/cofix.Emilio Jesus Gallego Arias
2018-03-09Merge PR #6820: Tacticals assert_fails and assert_succeedsMaxime Dénès
2018-03-09Merge PR #6155: Get rid of ' notation for Zpos in QArithMaxime Dénès
2018-03-09Merge PR #6937: Add empty compat file for Coq 8.8Maxime 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-08Merge PR #6909: Deprecate Focus and UnfocusMaxime Dénès
2018-03-07[stdlib] Do not use “Require” inside sectionsVincent Laporte
2018-03-07Add empty compat file for Coq 8.8Jason Gross
2018-03-07Merge PR #6744: Add String.concatMaxime Dénès
2018-03-05Merge PR #6855: Update headers following #6543.Maxime Dénès
2018-03-04Remove all uses of Focus in standard library.Théo Zimmermann
2018-03-02Remove 8.5 compatibility support.Théo Zimmermann
2018-03-02Remove VOld compatibility flag.Théo Zimmermann
2018-03-02Turn warning for deprecated notations on.Théo Zimmermann
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-28Merge PR #6852: [stdlib] move “Require” out of sectionsMaxime Dénès
2018-02-28Merge PR #1026: changed statements of Rpower_lt and Rle_power and added lemmasMaxime Dénès
2018-02-27Update headers following #6543.Théo Zimmermann
2018-02-27[stdlib] move “Require” out of sectionsVincent Laporte
2018-02-24Add String.concatJason Gross
2018-02-24Merge PR #6599: Decimals in preludeMaxime Dénès
2018-02-21Merge PR #6282: proposed fix for issue #3213: extra variable m in Lt.S_predMaxime Dénès
2018-02-20Decimal goodies : conversion to/from Coq stringsPierre Letouzey
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-20More structured printing in unicode notations for binders.Hugo Herbelin
2018-02-20User-level support for Gonthier-Ssreflect's "if t then pat then u else v".Hugo Herbelin
2018-02-19Merge PR #6556: Remove dir-locals and ship suggested helper hooks instead.Maxime Dénès
2018-02-12Add notation {x & P} for sigTTej Chajed
2018-02-12Merge PR #6139: Make list functions returning sumbools transparentMaxime Dénès
2018-01-08Document between and exists_between types.Ismail
2018-01-06Remove dir-locals and ship suggested helper hooks instead.Gaëtan Gilbert
2018-01-03Fix core hint database issue #6521Anton Trunov
2017-12-19Fix warning about shadowing a global name.Gaëtan Gilbert
2017-12-14Add named timers to LtacProfJason Gross
2017-12-12Merge PR #6335: Additional rewrite lemmas on Ensembles, in Powerset_factsMaxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-22 03:44:33 +0000