| Age | Commit message (Expand) | Author |
|---|---|---|
| 2012-08-08 | Updating headers. | herbelin |
| 2012-06-22 | Added an indirection with respect to Loc in Compat. As many [open Compat] | ppedrot |
| 2012-03-23 | Remove old proof-managment commands Suspend/Resume | letouzey |
| 2012-03-14 | Integrated obligations/eterm and program well-founded fixpoint building to to... | msozeau |
| 2012-03-02 | Noise for nothing | pboutill |
| 2011-12-12 | Proof using ... | gareuselesinge |
| 2011-05-17 | Break circular dependency Proof_global -> Vernacexpr -> Proof_global. | aspiwack |
| 2011-05-13 | New option [Set Bullet Behavior] allows to select the behaviour of bullets. | aspiwack |
| 2011-04-29 | Some comments. | aspiwack |
| 2011-02-10 | Started to fix the declarative proof mode (C-zar). | aspiwack |
| 2010-07-24 | Updated all headers for 8.3 and trunk | herbelin |
| 2010-05-05 | Pfedit.resume_proof doesn't implicitly Pfedit.suspend_proof | pboutill |
| 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 |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |