aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/nsatz/Nsatz.v
Commit message (Expand)AuthorAge
* [stdlib] Do not use “Require” inside sectionsGravatar Vincent Laporte2018-03-07
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* Fix nsatz not recognizing real literals.Gravatar Guillaume Melquiond2017-04-20
* Bug fix : variable capture in ltac code of NsatzGravatar thery2016-07-05
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
* Update headers.Gravatar Maxime Dénès2015-01-12
* Fixing an incompleteness of the ring/field tacticsGravatar amahboub2013-08-23
* Little fix for Nsatz: hypotheses not directly relevant to the nsatzGravatar herbelin2013-05-05
* Unset Asymmetric PatternsGravatar pboutill2013-01-18
* Updating headers.Gravatar herbelin2012-08-08
* More cleanup in Ring_polynom and EnvRingGravatar letouzey2012-07-05
* ZArith + other : favor the use of modern names instead of compat notationsGravatar letouzey2012-07-05
* moins de reification inutile, noatations standardsGravatar pottier2011-08-04
* Ring2 devient Ncring et la reification par les type classes est partageeGravatar pottier2011-07-26
* Tests de nsatz avec la geometrieGravatar pottier2011-06-16
* ring2, cring, nsatz avec type classe avec parametres plus notationsGravatar pottier2011-06-10
* Some more revision of {P,N,Z}Arith + bitwise ops in NdigitsGravatar letouzey2010-11-18
* unification des tactiques nsatz pour R Z avec celle des anneaux integresGravatar pottier2010-07-28