aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Reals/Ranalysis_reg.v
Commit message (Expand)AuthorAge
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* Removing "intro" from the tactic AST.Gravatar Pierre-Marie Pédrot2016-06-03
* Making parentheses mandatory in tactic scopes.Gravatar Pierre-Marie Pédrot2016-03-04
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
* Update headers.Gravatar Maxime Dénès2015-01-12
* Change an axiom into a definition.Gravatar Guillaume Melquiond2014-09-17
* Updating headers.Gravatar herbelin2012-08-08
* Open Local Scope ---> Local Open Scope, same with Notation and aliiGravatar letouzey2012-07-05
* These files are displaced from Rtrigo.v and Ranalysis_reg.vGravatar bertot2012-06-11