aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Sorting
Commit message (Expand)AuthorAge
* Giving a more natural semantics to injection by default.Gravatar Hugo Herbelin2016-06-18
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\
* | Stronger invariants on the use of the introduction pattern (pat1,...,patn).Gravatar Hugo Herbelin2016-01-21
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
|/
* Remove some outdated files and fix permissions.Gravatar Guillaume Melquiond2015-07-31
* Update headers.Gravatar Maxime Dénès2015-01-12
* Avoid using a deprecated lemma in the standard library.Gravatar Guillaume Melquiond2014-06-26
* Make standard library independent of the names generated byGravatar Hugo Herbelin2014-06-04
* Making those proofs which depend on names generated for the argumentsGravatar Hugo Herbelin2014-06-01
* Now parsing rules of ML-declared tactics are only made available after theGravatar Pierre-Marie Pédrot2014-05-12
* - Fix bug preventing apply from unfolding Fixpoints.Gravatar Matthieu Sozeau2014-05-06
* Correct rebase on STM code. Thanks to E. Tassi for help on dealing withGravatar Matthieu Sozeau2014-05-06
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* FinFun.v: results about injective/surjective/bijective fonctions over finite ...Gravatar Pierre Letouzey2014-02-07
* Making the behavior of "injection ... as ..." more natural:Gravatar herbelin2013-06-02
* Updating headers.Gravatar herbelin2012-08-08
* isolate instances about Permutation and PermutationA which may slow rewriteGravatar letouzey2012-07-10
* induction/destruct : nicer syntax for generating equations (solves #2741)Gravatar letouzey2012-07-09
* Kills the useless tactic annotations "in |- *"Gravatar letouzey2012-07-05
* ZArith + other : favor the use of modern names instead of compat notationsGravatar letouzey2012-07-05
* Permutation: remove a compatibility notation which doesn't help MathClassesGravatar letouzey2012-05-22
* List + Permutation : more results about nth_error and nthGravatar letouzey2012-05-18
* theories/, plugins/ and test-suite/ ported to the Arguments vernacularGravatar gareuselesinge2011-11-21
* Omega: for non-arithmetical goals, try proving False from context (wish #2236)Gravatar letouzey2011-09-16
* Simplify proofs in Permutation using generalized rewriting.Gravatar msozeau2011-03-04
* Remove obsolete TheoryListGravatar glondu2011-02-10
* In passing, very quick uniformization of coqdoc headers in a few files.Gravatar herbelin2010-12-09
* Fixing coqdoc pretty-printing of a table in Mergesort. Incidentally,Gravatar herbelin2010-12-04
* Rewrite Heap merging so that it extracts to an O(n log n) definition.Gravatar msozeau2010-07-28
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Sorting library: export as hints only lemmas that obviously simplifyGravatar herbelin2010-07-02
* Made option "Automatic Introduction" active by default before too manyGravatar herbelin2010-06-08
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Uniformisation Sorting/Mergesort and Structures/OrdersGravatar letouzey2010-02-16
* Update CHANGES, add documentation for new commands/tactics and do a bitGravatar msozeau2010-01-30
* Addition of mergesort + cleaning of the Sorting libraryGravatar herbelin2009-12-13
* Factorisation between Makefile and ocamlbuild systems : .vo to compile are in...Gravatar letouzey2009-12-09
* Sorting/Permutation: no need to require the whole Arith (and hence plugins li...Gravatar letouzey2009-11-02
* Merge SetoidList2 into SetoidList.Gravatar letouzey2009-10-19
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* - Add more precise error localisation when one of the application failsGravatar herbelin2009-08-04
* Coq.Relations.Relations can move back to its short nameGravatar letouzey2008-03-19
* Suppress some warnings by writing ugly Coq.Relations.Relations in some .vGravatar letouzey2008-03-14
* Plug the new setoid implemtation in, leaving the original one commentedGravatar msozeau2008-03-06
* migration from Set to Type of FSet/FMap + some dependencies...Gravatar letouzey2008-03-04
* small tactics "swap" and "absurd_hyp" are now obsolete: "contradict" is Gravatar letouzey2007-11-06
* eqlistA is now equivlistAGravatar letouzey2007-06-27
* some more properties of fold and elements in FSetPropertiesGravatar letouzey2007-06-08
* Mise en forme des theoriesGravatar notin2006-10-17
* Changement de précédence de l'argument du by de assert; conséquences...Gravatar herbelin2006-05-23
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-23 07:29:35 +0000