aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/NArith/Ndigits.v
Commit message (Expand)AuthorAge
* Merge PR #6855: Update headers following #6543.Gravatar Maxime Dénès2018-03-05
|\
* | Remove the deprecation for some 8.2-8.5 compatibility aliases.Gravatar Théo Zimmermann2018-03-02
| * Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
|/
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
* Update headers.Gravatar Maxime Dénès2015-01-12
* Arith: full integration of the "Numbers" modular frameworkGravatar Pierre Letouzey2014-07-09
* Unset Asymmetric PatternsGravatar pboutill2013-01-18
* nat_iter n f x -> nat_rect _ x (fun _ => f) nGravatar pboutill2012-12-21
* Updating headers.Gravatar herbelin2012-08-08
* ZArith + other : favor the use of modern names instead of compat notationsGravatar letouzey2012-07-05
* Notation: a new annotation "compat 8.x" extending "only parsing"Gravatar letouzey2012-07-05
* Cleanup of NdigitsGravatar letouzey2011-06-30
* Modularization of BinNat + fixes of stdlibGravatar letouzey2011-05-05
* Vectors fully use implicit argumentsGravatar pboutill2011-02-10
* Numbers: simplier spec for testbitGravatar letouzey2011-01-20
* Ndigits: a Pshiftl_nat used in BigN (was double_digits there)Gravatar letouzey2011-01-04
* Cosmetic : let's take advantage of the n-ary exists notationGravatar letouzey2010-12-17
* First release of Vector library.Gravatar pboutill2010-12-10
* Numbers and bitwise functions.Gravatar letouzey2010-12-06
* Some more revision of {P,N,Z}Arith + bitwise ops in NdigitsGravatar letouzey2010-11-18
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Reverted 13293 commited mistakenly. Sorry for the noise.Gravatar herbelin2010-07-18
* Tentative de suppression de l'import automatique des hints et coercions.Gravatar herbelin2010-07-18
* Made option "Automatic Introduction" active by default before too manyGravatar herbelin2010-06-08
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Kill some useless dependencies (Bvector, Program.Syntax)Gravatar letouzey2010-02-17
* Remove various useless {struct} annotationsGravatar letouzey2009-11-02
* Init/Tactics.v: tactic with nicer name 'exfalso' for 'elimtype False'Gravatar letouzey2009-10-08
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* - Temptative change to notations like "as [|n H]_eqn" or "as [|n H]_eqn:H",Gravatar herbelin2009-01-02
* Fixes and refinements regarding occurrence selection:Gravatar herbelin2008-10-26
* Expérience de simplification de Ndigits compte tenu des tactiques existantGravatar herbelin2008-10-18
* In agreement with Laurent Thery, start migration of auxiliary results Gravatar letouzey2007-11-01
* suite du pont entre Bvector et NGravatar letouzey2006-04-26
* Un gros coup de lifting pour IntMap: Gravatar letouzey2006-04-25