| Age | Commit message (Expand) | Author |
|---|
| 2011-07-26 | All the parameters of or can be implicits. | pboutill |
| 2011-07-26 | Same Implicit Arguments rule for sumbool and sumor. | pboutill |
| 2011-07-16 | Tentative abbreviation "rew Heq in H" for eq_rect. (feedback welcome) | herbelin |
| 2011-07-16 | Added a characterization of unique existence. | herbelin |
| 2011-06-20 | Arithemtic: more concerning compare, eqb, leb, ltb | letouzey |
| 2011-06-20 | Some simplifications in NZDomain | letouzey |
| 2011-05-05 | Wf.iter_nat becomes Peano.nat_iter (with an implicit arg) | letouzey |
| 2011-05-05 | Modularization of BinNat + fixes of stdlib | letouzey |
| 2011-05-05 | Better comments and organisation in Datatypes.v | letouzey |
| 2011-04-28 | Fixing an "apply -> ... in hyp" bug (the hyp was considered as a fixed | herbelin |
| 2011-03-21 | Init: some results in Type should rather be Defined than Qed | letouzey |
| 2011-03-17 | CompareSpec: a slight generalization/reformulation of CompSpec | letouzey |
| 2011-01-28 | Remove the "Boxed" syntaxes and the const_entry_boxed field | letouzey |
| 2010-12-10 | First release of Vector library. | pboutill |
| 2010-10-23 | Used multiple lists of implicit arguments to transfer the choices of | herbelin |
| 2010-10-03 | Using multiple lists of implicit arguments in Program for preserving | herbelin |
| 2010-07-24 | Updated all headers for 8.3 and trunk | herbelin |
| 2010-07-22 | Made notations for exists, exists! and notations of Utf8.v recursive notations | herbelin |
| 2010-07-16 | Bool: shorter and more systematic proofs + an iff lemma about eqb | letouzey |
| 2010-07-10 | Bool: iff lemmas about or, a reflect inductive, an is_true function | letouzey |
| 2010-06-18 | clear/revert dependent: restrict to hyp(h) instead of ident(h) | letouzey |
| 2010-06-17 | New tactic "clear dependent", for the moment in ltac in Init/Tactics | letouzey |
| 2010-04-29 | Remove the svn-specific $Id$ annotations | letouzey |
| 2010-04-22 | Here comes the commit, announced long ago, of the new tactic engine. | aspiwack |
| 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 |
