| Commit message (Expand) | Author | Age |
|---|
| * | Init: some results in Type should rather be Defined than Qed |  letouzey | 2011-03-21 |
| * | CompareSpec: a slight generalization/reformulation of CompSpec | letouzey | 2011-03-17 |
| * | Remove the "Boxed" syntaxes and the const_entry_boxed field | letouzey | 2011-01-28 |
| * | First release of Vector library. |  pboutill | 2010-12-10 |
| * | Used multiple lists of implicit arguments to transfer the choices of |  herbelin | 2010-10-23 |
| * | Using multiple lists of implicit arguments in Program for preserving | herbelin | 2010-10-03 |
| * | Updated all headers for 8.3 and trunk | herbelin | 2010-07-24 |
| * | Made notations for exists, exists! and notations of Utf8.v recursive notations | herbelin | 2010-07-22 |
| * | Bool: shorter and more systematic proofs + an iff lemma about eqb | letouzey | 2010-07-16 |
| * | Bool: iff lemmas about or, a reflect inductive, an is_true function | letouzey | 2010-07-10 |
| * | clear/revert dependent: restrict to hyp(h) instead of ident(h) | letouzey | 2010-06-18 |
| * | New tactic "clear dependent", for the moment in ltac in Init/Tactics | letouzey | 2010-06-17 |
| * | Remove the svn-specific $Id$ annotations | letouzey | 2010-04-29 |
| * | Here comes the commit, announced long ago, of the new tactic engine. |  aspiwack | 2010-04-22 |
| * | Arith's min and max placed in Peano (+basic specs max_l and co) | letouzey | 2010-02-17 |
| * | CompSpec2Type is used to build functions, it should be Defined, not Qed | letouzey | 2010-02-13 |
| * | CompSpecType, a clone of CompSpec but in Type instead of Prop | letouzey | 2010-02-12 |
| * | Init/Logic: commutativity and associativity of /\ and \/ | letouzey | 2010-01-08 |
| * | Factorisation between Makefile and ocamlbuild systems : .vo to compile are in... | letouzey | 2009-12-09 |
| * | Some lemmas about dependent choice + extensions of Compare_dec + | herbelin | 2009-11-16 |
| * | Datatypes.length and app defined back via fun+fix instead of Fixpoint | letouzey | 2009-11-06 |
| * | Better visibility of the inductive CompSpec used to specify comparison functions | letouzey | 2009-11-03 |
| * | Remove various useless {struct} annotations | letouzey | 2009-11-02 |
| * | list, length, app are migrated from List to Datatypes | letouzey | 2009-11-02 |
| * | 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-10-08 |
| * | Delete trailing whitespaces in all *.{v,ml*} files |  glondu | 2009-09-17 |
| * | New tactic to rewrite decidability lemmas when one knows which side | herbelin | 2009-08-24 |
| * | Fixed extra space in printing notation { x & P } + minor other things | herbelin | 2009-08-11 |
| * | OrderedTypeEx.N_as_OT use Nlt, various minor improvements in N/ZArith | letouzey | 2009-07-24 |
| * | Miscellaneous practical commits: | herbelin | 2009-06-29 |
| * | Parsing files for numerals (+ ascii/string) moved into plugins | letouzey | 2009-03-27 |
| * | Better mechanism for loading initial plugins | letouzey | 2009-03-14 |
| * | - Temptative change to notations like "as [|n H]_eqn" or "as [|n H]_eqn:H", | herbelin | 2009-01-02 |
| * | Switched to "standardized" names for the properties of eq and | herbelin | 2009-01-01 |
| * | - Another bug in get_sort_family_of (sort-polymorphism of constants and | herbelin | 2008-12-28 |
| * | - 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-12-26 |
| * | Fine-tuning rewriting from "eq_true b": using <- to rewrite true to b | herbelin | 2008-11-23 |
| * | - Fixed minor bug #1994 in the tactic chapter of the manual [doc] | herbelin | 2008-11-22 |
| * | ugly comment erroneously left in the minus definition | letouzey | 2008-10-14 |
| * | Correction de bugs: | herbelin | 2008-08-05 |
| * | Évolutions diverses et variées. | herbelin | 2008-08-04 |
| * | Fixed doc of inductive sort-polymorphism (cf bug #1908). Seized the | herbelin | 2008-07-23 |
| * | Changing the definitions of pred and minus in the style of GG |  werner | 2008-06-12 |
| * | - Patch sur "intros until 0" | herbelin | 2008-06-08 |
| * | - Extension de "generalize" en "generalize c as id at occs". | herbelin | 2008-06-08 |
| * | Petites corrections diverses : | herbelin | 2008-06-02 |
| * | - 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-28 |
letouzey
pboutill
herbelin
aspiwack
glondu
werner