aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Numbers
Commit message (Expand)AuthorAge
* Splitting primitive numeral parser/printer for positive, N, Z into three files.Gravatar Hugo Herbelin2018-06-29
* 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
|/
* Decimal goodies : conversion to/from Coq stringsGravatar Pierre Letouzey2018-02-20
* Decimal: proofs that conversions from/to nat,N,Z are bijectionsGravatar Pierre Letouzey2018-02-20
* Ensuring all .v files end with a newline to make "sed -i" work better on them.Gravatar Hugo Herbelin2017-08-21
* Merge PR #845: Add Z.mod_div lemma to standard library.Gravatar Maxime Dénès2017-07-26
|\
* | Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
| * Add Z.mod_div lemma to standard library.Gravatar Russell O'Connor2017-06-29
|/
* BigNums: remove files about BigN,BigZ,BigQ (now in an separate git repo)Gravatar Pierre Letouzey2017-06-13
* drop vo.itarget files and compute the corresponding the corresponding values ...Gravatar Matej Kosik2017-06-01
* Fix some documentation typos.Gravatar Guillaume Melquiond2016-11-24
* ZDivEucl: notations in different scope to avoid a warningGravatar Pierre Letouzey2016-09-28
* Extending "contradiction" so that it recognizes statements such as "~x=x" or ...Gravatar Hugo Herbelin2016-09-15
* Giving a more natural semantics to injection by default.Gravatar Hugo Herbelin2016-06-18
* Remove unneded hints in NZGcdGravatar Matthieu Sozeau2016-06-16
* Typeclasses: stdlib fixes for new search algorithmGravatar Matthieu Sozeau2016-06-16
* In NMake_gen, giving to tactic do_size a grammar rule which respects the levels.Gravatar Hugo Herbelin2016-06-16
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-05-09
|\
| * NPeano : improve compatibility for this deprecated file via compat notationsGravatar Pierre Letouzey2016-05-04
* | Revert "In NMake_gen, giving to tactic do_size a grammar rule which respects ...Gravatar Hugo Herbelin2016-04-27
* | In NMake_gen, giving to tactic do_size a grammar rule which respects the levels.Gravatar Hugo Herbelin2016-04-27
* | Making parentheses mandatory in tactic scopes.Gravatar Pierre-Marie Pédrot2016-03-04
* | Qcanon : implement some old suggestions by C. AugerGravatar Pierre Letouzey2016-02-26
|/
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
* Fix some typos.Gravatar Guillaume Melquiond2015-12-07
* Fix some typos.Gravatar Guillaume Melquiond2015-10-13
* Update headers.Gravatar Maxime Dénès2015-01-12
* Failing on unbound notation variable in notation level modifiersGravatar Hugo Herbelin2014-12-15
* Enforcing a stronger difference between the two syntaxes "simplGravatar Hugo Herbelin2014-11-16
* Revert d0cd27e209be08ee51a2d609157367f053438a10: giving a different nameGravatar Matthieu Sozeau2014-10-11
* Give the same argument name for the record binder of type classGravatar Matthieu Sozeau2014-10-10
* Fix segfault in native compiler on int31 division.Gravatar Maxime Dénès2014-10-10
* argument flip of Cyclic31.nshiftr and Cyclic31.nshiftlGravatar Pierre Boutillier2014-10-01
* Simpl less (so that cbn will not simpl too much)Gravatar Pierre Boutillier2014-10-01
* Keyed unification option, compiling the whole standard libraryGravatar Matthieu Sozeau2014-09-27
* - Fix printing and parsing of primitive projections, including the SetGravatar Matthieu Sozeau2014-09-09
* "allows to", like "allowing to", is improperGravatar Jason Gross2014-08-25
* instanciation is French, instantiation is EnglishGravatar Jason Gross2014-08-25
* Arith: full integration of the "Numbers" modular frameworkGravatar Pierre Letouzey2014-07-09
* Fixing bug #3270. Patch by Robbert Krebbers.Gravatar Pierre-Marie Pédrot2014-07-08
* Making those proofs which depend on names generated for the argumentsGravatar Hugo Herbelin2014-06-01
* Moving (e)transitivity out of the AST.Gravatar Pierre-Marie Pédrot2014-05-20
* - Fix treatment of global universe constraints which should be passed alongGravatar Matthieu Sozeau2014-05-06
* Restore reasonable performance by not allocating during universe checks,Gravatar Matthieu Sozeau2014-05-06
* - Rename eq to equal in Univ, document new modules, set interfaces.Gravatar Matthieu Sozeau2014-05-06
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Pos.iter arguments in a better order for cbn.Gravatar Pierre Boutillier2014-05-02
* "Boolean Equality" and "Case Analysis" are already off by default...Gravatar letouzey2013-07-17
generated by cgit v1.2.3 (git 2.39.1) at 2024-04-30 16:14:53 +0000