aboutsummaryrefslogtreecommitdiff
path: root/theories
AgeCommit message (Expand)Author
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
2017-12-11Axiom-free proof of eta expansion.Jasper Hugunin
2017-12-09Remove most uses of function extensionality in Program.CombinatorsJasper Hugunin
2017-12-06Additional rewrite lemmas on Ensembles, in Powerset_factsJoachim Breitner
2017-12-01proposed fix for issue #3213: extra variable m in Lt.S_predfredokun
2017-11-28Fix (partial) #4878: option to stop autodeclaring axiom as instance.Gaëtan Gilbert
2017-11-15Make list functions returning sumbools transparentTej Chajed
2017-11-14Get rid of ' notation for Zpos in QArith.Robbert Krebbers
2017-10-27Merge PR #1113: Adding 3 Arith/QArith lemmas that I found usefulMaxime Dénès
2017-10-27Chaining two tactics in a proofRaphaël Monat
2017-10-25Moving from `is_true` to `= true`Raphaël Monat
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-25 13:43:16 +0000