| Age | Commit message (Expand) | Author |
|---|
| 2010-02-17 | Arith's min and max placed in Peano (+basic specs max_l and co) | letouzey |
| 2010-02-13 | CompSpec2Type is used to build functions, it should be Defined, not Qed | letouzey |
| 2010-02-12 | CompSpecType, a clone of CompSpec but in Type instead of Prop | letouzey |
| 2010-01-08 | Init/Logic: commutativity and associativity of /\ and \/ | letouzey |
| 2009-12-09 | Factorisation between Makefile and ocamlbuild systems : .vo to compile are in... | letouzey |
| 2009-11-16 | Some lemmas about dependent choice + extensions of Compare_dec + | herbelin |
| 2009-11-06 | Datatypes.length and app defined back via fun+fix instead of Fixpoint | letouzey |
| 2009-11-03 | Better visibility of the inductive CompSpec used to specify comparison functions | letouzey |
| 2009-11-02 | Remove various useless {struct} annotations | letouzey |
| 2009-11-02 | list, length, app are migrated from List to Datatypes | letouzey |
| 2009-10-08 | Init/Tactics.v: tactic with nicer name 'exfalso' for 'elimtype False' | letouzey |
| 2009-10-08 | Implicit argument of Logic.eq become maximally inserted | letouzey |
| 2009-09-17 | Delete trailing whitespaces in all *.{v,ml*} files | glondu |
| 2009-08-24 | New tactic to rewrite decidability lemmas when one knows which side | herbelin |
| 2009-08-11 | Fixed extra space in printing notation { x & P } + minor other things | herbelin |
| 2009-07-24 | OrderedTypeEx.N_as_OT use Nlt, various minor improvements in N/ZArith | letouzey |
| 2009-06-29 | Miscellaneous practical commits: | herbelin |
| 2009-03-27 | Parsing files for numerals (+ ascii/string) moved into plugins | letouzey |
| 2009-03-14 | Better mechanism for loading initial plugins | letouzey |
| 2009-01-02 | - Temptative change to notations like "as [|n H]_eqn" or "as [|n H]_eqn:H", | herbelin |
| 2009-01-01 | Switched to "standardized" names for the properties of eq and | herbelin |
| 2008-12-28 | - Another bug in get_sort_family_of (sort-polymorphism of constants and | herbelin |
| 2008-12-26 | - Extracted from the tactic "now" an experimental tactic "easy" for small | herbelin |
| 2008-12-26 | - Optimized "auto decomp" which had a (presumably) exponential in | herbelin |
| 2008-11-23 | Fine-tuning rewriting from "eq_true b": using <- to rewrite true to b | herbelin |
| 2008-11-22 | - Fixed minor bug #1994 in the tactic chapter of the manual [doc] | herbelin |
| 2008-10-14 | ugly comment erroneously left in the minus definition | letouzey |
| 2008-08-05 | Correction de bugs: | herbelin |
| 2008-08-04 | Évolutions diverses et variées. | herbelin |
| 2008-07-23 | Fixed doc of inductive sort-polymorphism (cf bug #1908). Seized the | herbelin |
| 2008-06-12 | Changing the definitions of pred and minus in the style of GG | werner |
| 2008-06-08 | - Patch sur "intros until 0" | herbelin |
| 2008-06-08 | - Extension de "generalize" en "generalize c as id at occs". | herbelin |
| 2008-06-02 | Petites corrections diverses : | herbelin |
| 2008-05-28 | - Modification de la déf de minus et pred conformément aux remarques de | herbelin |
| 2008-05-28 | Notation concise pour la valeur par défaut des cas reconnus comme | herbelin |
| 2008-05-12 | MAJ et bricoles diverses | herbelin |
| 2008-05-09 | Backtrack sur la mise à disposition en standard de la notation [ x ; ... ; y ] | herbelin |
| 2008-04-29 | Ajout notation [ x ; ... ; y ] dans list_scope. Changement de la | herbelin |
| 2008-04-23 | Prise en compte des coercions dans les clauses "with" même si le type | herbelin |
| 2008-04-09 | contradict can now handle False hypothesis in the spirit of contradiction | letouzey |
| 2008-03-23 | Nettoyage Wf.v et unification (suite remarques faites sur cocorico) | herbelin |
| 2008-03-23 | Une passe sur les réels: | herbelin |
| 2008-03-15 | Do a second pass on the treatment of user-given implicit arguments. Now | msozeau |
| 2008-03-07 | f_equal, revert, specialize in ML, contradict in better Ltac (+doc) | letouzey |
| 2008-03-04 | still one more substituion s/Set/Type/ | letouzey |
| 2008-02-26 | Proper implicit arguments handling for assumptions | msozeau |
| 2008-01-23 | Typo | notin |
| 2007-12-17 | Quelques arguments en plus... | glondu |
| 2007-11-08 | Moved several lemmas from theories/Numbers/NumPrelude to theories/Init/Logic. | emakarov |
