aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Numbers
Commit message (Expand)AuthorAge
* 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
* Change Hint Resolve, Immediate to take a global reference as argumentGravatar msozeau2012-10-26
* Ltac repeat is in fact already doing progressGravatar letouzey2012-10-01
* fast bitwise operations (lor,land,lxor) on int31 and BigNGravatar letouzey2012-08-11
* Updating headers.Gravatar herbelin2012-08-08
* induction/destruct : nicer syntax for generating equations (solves #2741)Gravatar letouzey2012-07-09
* ZArith + other : favor the use of modern names instead of compat notationsGravatar letouzey2012-07-05
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-16 15:26:12 +0000