aboutsummaryrefslogtreecommitdiff
path: root/theories/Init/Datatypes.v
AgeCommit message (Expand)Author
2020-11-16Explicitly annotate all hint declarations of the standard library.Pierre-Marie Pédrot
2020-08-20Modify Init/Datatypes.v to compile with -mangle-names.Jasper Hugunin
2020-08-11deprecate prod_curry and prod_uncurryYishuai Li
2020-06-14[micromega] native support for boolean operatorsFrédéric Besson
2020-05-15Merge PR #11948: Hexadecimal numeralsHugo Herbelin
2020-05-11Merge PR #10609: Register (for Coqlib.ref_lib) several base datatypes of stdlibHugo Herbelin
2020-05-09Add hexadecimal numeralsPierre Roux
2020-05-09Merge PR #11990: [micromega] use Coqlib.lib_ref to get Coq constants.Maxime Dénès
2020-04-21Moving the main Require Export Ltac in Prelude.v.Hugo Herbelin
2020-04-02chore: Add missing [Register] for inductive types in Datatypes.vThomas Letan
2020-04-01[micromega] use Coqlib.lib_ref to get Coq constants.Frédéric Besson
2020-03-18Update headers in the whole code base.Théo Zimmermann
2019-09-09Merge PR #9379: Vectors: lemmas about uncons and splitAtHugo Herbelin
2019-09-01edits per reviewYishuai Li
2019-09-01Vectors: lemmas about uncons and splitAtYishuai Li
2019-08-26Make kernel parametric on the lowest universe and fix #9294Matthieu Sozeau
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2018-12-19Put #[universes(template)] on all auto template spots in stdlibGaëtan Gilbert
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-09-25Adding lemmas about dependent equality.Hugo Herbelin
2018-09-25Mini refreshing layout Datatypes.v.Hugo Herbelin
2018-09-10Adapting standard library to the introduction of "Declare Scope".Hugo Herbelin
2018-08-31Numeral Notation for natPierre Letouzey
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-27Update headers following #6543.Théo Zimmermann
2017-07-05Fix typo in documentation for identityTej Chajed
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-04-25Give andb_prop a simpler proofJason Gross
2017-03-03A couple of other useful properties about compare_cont.Hugo Herbelin
2017-03-03Compatibility of iff wrt not and imp.Hugo Herbelin
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2015-05-09Tentatively setting cons and Some with 1st implicit argument maximalHugo Herbelin
2015-01-18Correct restriction of vm_compute when handling universe polymorphicMatthieu Sozeau
2015-01-15Correct restriction of vm_compute when handling universe polymorphicMatthieu Sozeau
2015-01-12Update headers.Maxime Dénès
2014-09-09- Fix printing and parsing of primitive projections, including the SetMatthieu Sozeau
2014-05-06Try a new way of handling template universe levelsMatthieu Sozeau
2014-05-06- Fix bug preventing apply from unfolding Fixpoints.Matthieu Sozeau
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-01-24[Coercion]s use [Sortclass], not [Prop] (in docs)Jason Gross
2012-08-08Updating headers.herbelin
2012-07-05Kills the useless tactic annotations "in |- *"letouzey
2012-07-05ZArith + other : favor the use of modern names instead of compat notationsletouzey
2012-01-19No more use of tauto in Init/pboutill
2011-11-21theories/, plugins/ and test-suite/ ported to the Arguments vernaculargareuselesinge
2011-06-20Arithemtic: more concerning compare, eqb, leb, ltbletouzey
2011-05-05Modularization of BinNat + fixes of stdlibletouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 11:13:21 +0000