index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
theories
/
Numbers
/
NatInt
/
NZSqrt.v
Age
Commit message (
Expand
)
Author
2020-08-25
Modify Numbers/NatInt/NZSqrt.v to compile with -mangle-names
Jasper Hugunin
2020-03-18
Update headers in the whole code base.
Théo Zimmermann
2019-06-17
Update ml-style headers to new year.
Théo Zimmermann
2019-01-23
Pass some files to strict focusing mode.
Gaëtan Gilbert
2018-02-27
Update headers following #6543.
Théo Zimmermann
2017-07-04
Bump year in headers.
Pierre-Marie Pédrot
2016-01-20
Update copyright headers.
Maxime Dénès
2015-01-12
Update headers.
Maxime Dénès
2014-05-20
Moving (e)transitivity out of the AST.
Pierre-Marie Pédrot
2014-05-06
This commit adds full universe polymorphism and fast projections to Coq.
Matthieu Sozeau
2012-08-08
Updating headers.
herbelin
2011-01-04
f_equiv : a clone of f_equal that handles setoid equivalences
letouzey
2011-01-03
Numbers: some improvements in proofs
letouzey
2010-11-18
NZSqrt: we define sqrt_up, a square root that rounds up instead of down as sqrt
letouzey
2010-11-02
NZSqrt : since spec is complete, no need for morphism axiom sqrt_wd
letouzey
2010-11-02
Numbers: misc improvements
letouzey
2010-11-02
Numbers: specs about sqrt and pow of neg numbers, even in NZ
letouzey
2010-11-02
Numbers: NZPowProp as a Module Type, some module variable renaming
letouzey
2010-10-19
Add sqrt in Numbers
letouzey