| Age | Commit message (Expand) | Author |
|---|---|---|
| 2010-02-17 | Kill some useless dependencies (Bvector, Program.Syntax) | letouzey |
| 2009-11-02 | Remove various useless {struct} annotations | letouzey |
| 2009-10-08 | Init/Tactics.v: tactic with nicer name 'exfalso' for 'elimtype False' | letouzey |
| 2009-09-17 | Delete trailing whitespaces in all *.{v,ml*} files | glondu |
| 2009-01-02 | - Temptative change to notations like "as [|n H]_eqn" or "as [|n H]_eqn:H", | herbelin |
| 2008-10-26 | Fixes and refinements regarding occurrence selection: | herbelin |
| 2008-10-18 | Expérience de simplification de Ndigits compte tenu des tactiques existant | herbelin |
| 2007-11-01 | In agreement with Laurent Thery, start migration of auxiliary results | letouzey |
| 2006-04-26 | suite du pont entre Bvector et N | letouzey |
| 2006-04-25 | Un gros coup de lifting pour IntMap: | letouzey |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |