aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Numbers
Commit message (Expand)AuthorAge
* 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
* More dynamic argument scopesGravatar letouzey2013-07-17
* NMake*: avoid some warning about Let outside sectionsGravatar letouzey2013-03-22
* make validate repaired via a temporary fix for #2949Gravatar letouzey2013-02-13
* nat_iter n f x -> nat_rect _ x (fun _ => f) nGravatar pboutill2012-12-21
* Rework of GenericMinMax and OrdersTac (helps extraction, cf. #2904)Gravatar letouzey2012-12-18
* Finish patch for Hint Resolve, stopping to generate new constant names forGravatar msozeau2012-12-08