| Commit message (Expand) | Author | Age |
* | Simpl less (so that cbn will not simpl too much) | Pierre Boutillier | 2014-10-01 |
* | instanciation is French, instantiation is English | Jason Gross | 2014-08-25 |
* | Grammar: "allowing to" is not proper English | Jason Gross | 2014-08-25 |
* | Avoid using a deprecated lemma in the standard library. | Guillaume Melquiond | 2014-06-26 |
* | Making those proofs which depend on names generated for the arguments | Hugo Herbelin | 2014-06-01 |
* | This commit adds full universe polymorphism and fast projections to Coq. | Matthieu Sozeau | 2014-05-06 |
* | Unset Asymmetric Patterns | pboutill | 2013-01-18 |
* | No more constant named "int" in Coq theories (cf bug #2878) | letouzey | 2012-12-18 |
* | Ltac repeat is in fact already doing progress | letouzey | 2012-10-01 |
* | Kills the useless tactic annotations "in |- *" | letouzey | 2012-07-05 |
* | Open Local Scope ---> Local Open Scope, same with Notation and alii | letouzey | 2012-07-05 |
* | Modularization of BinInt, related fixes in the stdlib | letouzey | 2011-05-05 |
* | - Use transparency information all the way through unification and | msozeau | 2011-02-17 |
* | s/appartness/membership/g (Closes: #2470) | glondu | 2011-01-06 |
* | Extraction: re-introduce some eta-expansions in rare situations leading to '_... | letouzey | 2010-09-20 |
* | For the moment, two small manual eta-expansions to avoid '_a after extraction | letouzey | 2010-09-17 |
* | Made option "Automatic Introduction" active by default before too many | herbelin | 2010-06-08 |
* | Remove the svn-specific $Id$ annotations | letouzey | 2010-04-29 |
* | Merge SetoidList2 into SetoidList. | letouzey | 2009-10-19 |
* | Structure/OrderTac.v : highlight the "order" tactic by isolating it from FSet... | letouzey | 2009-10-16 |
* | Fix the stdlib doc compilation + switch all .v file to utf8 | letouzey | 2009-09-28 |
* | Delete trailing whitespaces in all *.{v,ml*} files | glondu | 2009-09-17 |
* | made several occurrences of (eapply ...; eauto) not rely on the lack of patte... | barras | 2009-06-22 |
* | Intropattern: syntax {x,y,z,t} becomes (x & y & z & t), as decided in | letouzey | 2008-06-01 |
* | Prevent the apparition of &&& when printing a (if ... then ... else false) | letouzey | 2008-04-17 |
* | New file FMapFullAVL containing the balancing proofs about FMapAVL: | letouzey | 2008-04-03 |
* | Rework of FMapAVL inspired by recent changes of FSetAVL: | letouzey | 2008-04-03 |
* | Reorganisation of FSetAVL (consequences of remarks by B. Gregoire) | letouzey | 2008-03-15 |
* | repair FSets/FMap after the change in setoid rewrite | letouzey | 2008-03-07 |
* | migration from Set to Type of FSet/FMap + some dependencies... | letouzey | 2008-03-04 |
* | Some suggestions about FMap by P. Casteran: | letouzey | 2008-02-28 |
* | cardinal is promoted to the rank of primitive member of the FMap interface | letouzey | 2008-02-28 |
* | Major revision: use of Function, including some non-structural ones | letouzey | 2008-02-10 |
* | kill some useless module aliases E:=X (for better name printing, see Elie's 1... | letouzey | 2008-02-05 |
* | small tactics "swap" and "absurd_hyp" are now obsolete: "contradict" is | letouzey | 2007-11-06 |
* | Revision of the FSetWeak Interface, so that it becomes a precise | letouzey | 2007-10-29 |
* | A generic preprocessing tactic zify for (r)omega | letouzey | 2007-07-18 |
* | As suggested by Pierre Casteran, fold for FSets/FMaps now takes a | letouzey | 2007-05-27 |
* | fix for bug #1347 (no more Scope pollution by FSets) | letouzey | 2007-05-25 |
* | Passage des graphes de Function dans Type | jforest | 2006-06-23 |
* | + ameliorating the tactic "functional induction" | jforest | 2006-06-06 |
* | Replacing the old version of "functional induction" with the new one. | jforest | 2006-05-31 |
* | * suite de la revision des wrappers Make | letouzey | 2006-05-30 |
* | suite de l'ajout des FSets/FMaps dans les theories standards | letouzey | 2006-04-29 |