aboutsummaryrefslogtreecommitdiff
path: root/theories/Structures
AgeCommit message (Expand)Author
2019-10-31lia: depend only on ZArith_baseVincent Laporte
2019-10-22OrderedTypeEx: do not use “omega”Vincent Laporte
2019-10-04[Stdlib] OrderedType: do not pollute the “core” hint databaseVincent Laporte
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-05-23Fixing typos - Part 3JPR
2019-05-01Add PairUsualDecidableTypeFullOliver Nash
2019-03-30Error when [foo.(bar)] is used with nonprojection [bar]Gaëtan Gilbert
2019-01-23Pass some files to strict focusing mode.Gaëtan Gilbert
2018-12-10Merge PR #7221: The usual order of strings.Hugo Herbelin
2018-11-28Merge PR #7153: Make OrderedTypeFullFacts a module functorGaëtan Gilbert
2018-11-22The usual order of strings.Yao Li
2018-11-14Deprecate hint declaration/removal with no specified databaseMaxime Dénès
2018-09-10Adapting standard library to the introduction of "Declare Scope".Hugo Herbelin
2018-08-22Fix typo of caracterisation -> c*h*aracterisationSiddharth Bhat
2018-04-02Make OrderedTypeFullFacts a module functorSimon Gregersen
2018-03-05Merge PR #6855: Update headers following #6543.Maxime Dénès
2018-03-02Turn warning for deprecated notations on.Théo Zimmermann
2018-02-27Update headers following #6543.Théo Zimmermann
2017-06-01drop vo.itarget files and compute the corresponding the corresponding values ...Matej Kosik
2017-05-16Stop using auto with * in two proofs.Théo Zimmermann
2016-10-12Little addition to 6eede071 for consistency of style in OrdersFacts.v.Hugo Herbelin
2016-09-17Further "decide equality" tests on demand of Jason.Hugo Herbelin
2016-09-15Extending "contradiction" so that it recognizes statements such as "~x=x" or ...Hugo Herbelin
2016-04-27Revert "Temporary hack to compensate missing comma while re-printing tactic"Hugo Herbelin
2016-04-27Temporary hack to compensate missing comma while re-printing tacticHugo Herbelin
2016-01-13MMaps: remove it from final 8.5 release, since this new library isn't mature ...Pierre Letouzey
2015-12-31Put implicits back as in 8.4.Matthieu Sozeau
2015-12-07Fix some typos.Guillaume Melquiond
2015-03-06MMapPositive: another implementation of MMapsPierre Letouzey
2015-03-05MMaps again : adding MMapList, an implementation by ordered listPierre Letouzey
2015-03-04Introducing MMaps, a modernized FMaps.Pierre Letouzey
2014-08-25"allows to", like "allowing to", is improperJason Gross
2014-07-09Arith: full integration of the "Numbers" modular frameworkPierre Letouzey
2014-06-01Making those proofs which depend on names generated for the argumentsHugo Herbelin
2014-05-09Restore implicit arguments of irreflexivity (fixes bug #3305).Matthieu Sozeau
2014-05-06- Fix treatment of global universe constraints which should be passed alongMatthieu Sozeau
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2012-12-18Rework of GenericMinMax and OrdersTac (helps extraction, cf. #2904)letouzey
2012-07-09induction/destruct : nicer syntax for generating equations (solves #2741)letouzey
2012-07-05ZArith + other : favor the use of modern names instead of compat notationsletouzey
2012-04-15Fixing tauto "special" behavior on singleton types w/ 2 parameters (bug #2680).herbelin
2012-01-31Revert "Tentative to fix bug #2628 by not letting intuition break records. Mi...msozeau
2012-01-28Tentative to fix bug #2628 by not letting intuition break records. Might be t...msozeau
2011-11-21theories/, plugins/ and test-suite/ ported to the Arguments vernaculargareuselesinge
2011-08-11SearchAbout and similar: add a customizable blacklistletouzey
2011-07-26All the parameters of Compare are implicits.pboutill
2011-06-21Follow-up concerning eqb / ltb / leb comparisonsletouzey
2011-06-20Arithemtic: more concerning compare, eqb, leb, ltbletouzey
2011-05-05Modularization of BinInt, related fixes in the stdlibletouzey
2011-05-05Modularization of BinNat + fixes of stdlibletouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 13:42:06 +0000