aboutsummaryrefslogtreecommitdiff
path: root/theories/Init
AgeCommit message (Expand)Author
2020-11-22Adapting standard library, doc and test suite to ident->name renaming.Hugo Herbelin
2020-11-16Explicitly annotate all hint declarations of the standard library.Pierre-Marie Pédrot
2020-11-05Rename Dec and HexDec to Decimal and HexadecimalPierre Roux
2020-11-05Merge numeral and string notation pluginsPierre Roux
2020-11-05[numeral notation] QPierre Roux
2020-11-04[numeral notation] Adding the via ... using ... optionPierre Roux
2020-10-30Renaming Numeral.v into Number.vPierre Roux
2020-10-15Report a useful error for dependent destructionTej Chajed
2020-09-11Rename Numeral Notation command to Number NotationPierre Roux
2020-08-25Modify Classes/RelationClasses.v to compile with -mangle-namesJasper Hugunin
2020-08-25Modify Init/Tactics.v to compile with -mangle-namesJasper Hugunin
2020-08-25Modify Init/Wf.v to compile with -mangle-namesJasper Hugunin
2020-08-25Modify Init/Peano.v to compile with -mangle-names.Jasper Hugunin
2020-08-20Modify Init/Specif.v to compile with -mangle-namesJasper Hugunin
2020-08-20Modify Init/Datatypes.v to compile with -mangle-names.Jasper Hugunin
2020-08-20Modify Init/Logic.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-09Decimal: prove numeral notation for QPierre Roux
2020-05-09Merge PR #11990: [micromega] use Coqlib.lib_ref to get Coq constants.Maxime Dénès
2020-05-01Fixing #11903: Fixpoints not truly recursive in standard library.Hugo Herbelin
2020-04-21Moving the main Require Export Ltac in Prelude.v.Hugo Herbelin
2020-04-21Adding a Declare ML Module in empty file Ltac.v.Hugo Herbelin
2020-04-14Merge PR #11957: [stdlib] update sigma-type notationsHugo 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-30new sig notations and spaces addedOlivier Laurent
2020-03-28Remove SearchAbout command, deprecated in 8.5Jim Fehrle
2020-03-25Nicer printing for decimal constants in QPierre Roux
2020-03-19Merge PR #11822: Grants #11692: clear dependent knows about let-inPierre-Marie Pédrot
2020-03-18Update headers in the whole code base.Théo Zimmermann
2020-03-14Fixes #11692 (clear dependent knows about let-in).Hugo Herbelin
2020-03-06Fix #11738 : Funind using deprecated Coqlib API.Pierre Courtieu
2020-02-25Use implicit arguments in notations for eq.Gaëtan Gilbert
2020-02-19Choosing a standard format for the "rew dependent" notation.Hugo Herbelin
2019-12-26Add rew dependent NotationsJason Gross
2019-10-29Use a less kludgy way of solving #9114Jason Gross
2019-10-29Fix #9114, assert_succeeds (exact I) solves goalJason Gross
2019-10-29`assert_succeeds`&`assert_fails`: multisuccess fixJason Gross
2019-09-16Fix #10757: Program Fixpoint uses "exists" for telescopesGaëtan Gilbert
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
2019-05-25Modifying theories to preferably use the "[= ]" syntax, and,Hugo Herbelin
2019-05-23Fixing typos - Part 3JPR
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 09:41:30 +0000