aboutsummaryrefslogtreecommitdiff
path: root/theories/Arith
AgeCommit message (Expand)Author
2019-05-25Modifying theories to preferably use the "[= ]" syntax, and,Hugo Herbelin
2019-04-08Fix spelling in comment.nlewycky
2019-04-02Remove -compat 8.7Jason Gross
2018-10-10[coqlib] Rebindable Coqlib namespace.Emilio Jesus Gallego Arias
2018-10-02Update compat notations to be compat 8.7Jason Gross
2018-04-13[ltac] Deprecate nameless fix/cofix.Emilio Jesus Gallego Arias
2018-03-05Merge PR #6855: Update headers following #6543.Maxime Dénès
2018-03-02Remove the deprecation for some 8.2-8.5 compatibility aliases.Théo Zimmermann
2018-02-27Update headers following #6543.Théo Zimmermann
2018-02-24Merge PR #6599: Decimals in preludeMaxime Dénès
2018-02-21Merge PR #6282: proposed fix for issue #3213: extra variable m in Lt.S_predMaxime Dénès
2018-02-20Decimal: proofs that conversions from/to nat,N,Z are bijectionsPierre Letouzey
2018-01-08Document between and exists_between types.Ismail
2017-12-01proposed fix for issue #3213: extra variable m in Lt.S_predfredokun
2017-08-21Ensuring all .v files end with a newline to make "sed -i" work better on them.Hugo Herbelin
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-06-01drop vo.itarget files and compute the corresponding the corresponding values ...Matej Kosik
2017-01-30Proof clean-up.Théo Zimmermann
2016-10-24Remove v62 from stdlib.Théo Zimmermann
2016-06-18Giving a more natural semantics to injection by default.Hugo Herbelin
2016-01-20Update copyright headers.Maxime Dénès
2015-07-31Remove some outdated files and fix permissions.Guillaume Melquiond
2015-01-12Update headers.Maxime Dénès
2014-10-01Simpl less (so that cbn will not simpl too much)Pierre Boutillier
2014-07-22Fixed proof of irrelevance of le on nat, inspired by theMaxime Dénès
2014-07-09Arith: full integration of the "Numbers" modular frameworkPierre Letouzey
2014-06-01Making those proofs which depend on names generated for the argumentsHugo Herbelin
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2013-01-18Unset Asymmetric Patternspboutill
2012-12-21nat_iter n f x -> nat_rect _ x (fun _ => f) npboutill
2012-10-04Revert "En cours pour 'generalize in clause' et 'induction in clause'"herbelin
2012-10-04En cours pour 'generalize in clause' et 'induction in clause'herbelin
2012-08-08Updating headers.herbelin
2012-07-09induction/destruct : nicer syntax for generating equations (solves #2741)letouzey
2012-07-06Restore the compatibility notation Compare.not_eq_symletouzey
2012-07-05Kills the useless tactic annotations "in |- *"letouzey
2012-07-05Open Local Scope ---> Local Open Scope, same with Notation and aliiletouzey
2012-07-05ZArith + other : favor the use of modern names instead of compat notationsletouzey
2012-07-05Notation: a new annotation "compat 8.x" extending "only parsing"letouzey
2012-04-23remove undocumented and scarcely-used tactic auto decompletouzey
2011-11-21theories/, plugins/ and test-suite/ ported to the Arguments vernaculargareuselesinge
2011-09-17Euclid: make the proof transparent (example of extraction in stdlib)letouzey
2011-08-08Some forgotten lemma in Arith with "O" in the name instead of "0".herbelin
2011-05-05Wf.iter_nat becomes Peano.nat_iter (with an implicit arg)letouzey
2011-03-17CompareSpec: a slight generalization/reformulation of CompSpecletouzey
2011-01-28Remove the "Boxed" syntaxes and the const_entry_boxed fieldletouzey
2010-12-12Sorry for the mistake in r13702pboutill
2010-12-10First release of Vector library.pboutill
2010-11-18Some more revision of {P,N,Z}Arith + bitwise ops in Ndigitsletouzey
2010-10-21Solve name conflict about pow introduced by commit 13546.letouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-09 13:03:27 +0000