aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Arith
Commit message (Expand)AuthorAge
* Remove some outdated files and fix permissions.Gravatar Guillaume Melquiond2015-07-31
* Update headers.Gravatar Maxime Dénès2015-01-12
* Simpl less (so that cbn will not simpl too much)Gravatar Pierre Boutillier2014-10-01
* Fixed proof of irrelevance of le on nat, inspired by theGravatar Maxime Dénès2014-07-22
* Arith: full integration of the "Numbers" modular frameworkGravatar Pierre Letouzey2014-07-09
* Making those proofs which depend on names generated for the argumentsGravatar Hugo Herbelin2014-06-01
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Unset Asymmetric PatternsGravatar pboutill2013-01-18
* nat_iter n f x -> nat_rect _ x (fun _ => f) nGravatar pboutill2012-12-21
* Revert "En cours pour 'generalize in clause' et 'induction in clause'"Gravatar herbelin2012-10-04
* En cours pour 'generalize in clause' et 'induction in clause'Gravatar herbelin2012-10-04
* Updating headers.Gravatar herbelin2012-08-08
* induction/destruct : nicer syntax for generating equations (solves #2741)Gravatar letouzey2012-07-09
* Restore the compatibility notation Compare.not_eq_symGravatar letouzey2012-07-06
* Kills the useless tactic annotations "in |- *"Gravatar letouzey2012-07-05
* Open Local Scope ---> Local Open Scope, same with Notation and aliiGravatar letouzey2012-07-05
* ZArith + other : favor the use of modern names instead of compat notationsGravatar letouzey2012-07-05
* Notation: a new annotation "compat 8.x" extending "only parsing"Gravatar letouzey2012-07-05
* remove undocumented and scarcely-used tactic auto decompGravatar letouzey2012-04-23
* theories/, plugins/ and test-suite/ ported to the Arguments vernacularGravatar gareuselesinge2011-11-21
* Euclid: make the proof transparent (example of extraction in stdlib)Gravatar letouzey2011-09-17
* Some forgotten lemma in Arith with "O" in the name instead of "0".Gravatar herbelin2011-08-08
* Wf.iter_nat becomes Peano.nat_iter (with an implicit arg)Gravatar letouzey2011-05-05
* CompareSpec: a slight generalization/reformulation of CompSpecGravatar letouzey2011-03-17
* Remove the "Boxed" syntaxes and the const_entry_boxed fieldGravatar letouzey2011-01-28
* Sorry for the mistake in r13702Gravatar pboutill2010-12-12
* First release of Vector library.Gravatar pboutill2010-12-10
* Some more revision of {P,N,Z}Arith + bitwise ops in NdigitsGravatar letouzey2010-11-18
* Solve name conflict about pow introduced by commit 13546.Gravatar letouzey2010-10-21
* Add sqrt in NumbersGravatar letouzey2010-10-19
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Reverted 13293 commited mistakenly. Sorry for the noise.Gravatar herbelin2010-07-18
* Tentative de suppression de l'import automatique des hints et coercions.Gravatar herbelin2010-07-18
* Made option "Automatic Introduction" active by default before too manyGravatar herbelin2010-06-08
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Compare_dec : a few better proofs (and extracted terms), some more DefinedGravatar letouzey2010-04-16
* Arith's min and max placed in Peano (+basic specs max_l and co)Gravatar letouzey2010-02-17
* Min, Max: for avoiding inelegant NPeano.max printing, we Export this libGravatar letouzey2010-02-10
* Numbers: properties of min/max with respect to 0,S,P,add,sub,mulGravatar letouzey2010-02-09
* NPeano improved, subsumes NatOrderedTypeGravatar letouzey2010-02-09
* Simplification of OrdersTac thanks to the functor application ! with no inlineGravatar letouzey2010-01-17
* Nicer names: DecidableType2* --> Equalities*, OrderedType2* --> Orders*Gravatar letouzey2010-01-07
* Rework of GenericMinMax: new axiomatic, split logical/decidable parts, Leibni...Gravatar letouzey2010-01-07
* OrderTac: use TotalOrder, no more "change" before calling "order" (stuff with...Gravatar letouzey2010-01-07
* Reverse order of arguments in min_case_strong for better uniformity (and comp...Gravatar letouzey2009-12-17
* Factorisation between Makefile and ocamlbuild systems : .vo to compile are in...Gravatar letouzey2009-12-09
* Added support for definition of fixpoints using tactics.Gravatar herbelin2009-11-27
* Taking advantage of the new "Include Self Type" in DecidableType2 and NZAxiomsGravatar letouzey2009-11-16
* Some lemmas about dependent choice + extensions of Compare_dec +Gravatar herbelin2009-11-16
* DecidableType: A specification via boolean equality as an alternative to eq_decGravatar letouzey2009-11-10
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-27 13:25:23 +0000