| Commit message (Expand) | Author | Age | |
|---|---|---|---|
| * | Fixed subst failing when a truly heterogeneous JMeq hyp is in the |  herbelin | 2009-08-04 |
| * | Added "etransitivity". | herbelin | 2009-08-03 |
| * | - Allowing multiple calls to tactic fix with automatic generation of | herbelin | 2009-05-17 |
| * | Moved parts of Sign to Term. Unified some names (e.g. decomp_n_prod -> | herbelin | 2008-12-31 |
| * | - Fixed bugs and compatibilities issues in | herbelin | 2008-12-30 |
| * | - Another bug in get_sort_family_of (sort-polymorphism of constants and | herbelin | 2008-12-28 |
| * | - Optimized "auto decomp" which had a (presumably) exponential in | herbelin | 2008-12-26 |
| * | - Fixed minor bug #1994 in the tactic chapter of the manual [doc] | herbelin | 2008-11-22 |
| * | Uniformisation du format des messages d'erreur (commencent par une | herbelin | 2008-07-17 |
| * | - Déplacement des types paramétriques prod, sum, option, identity, | herbelin | 2006-05-28 |
| * | - Réintroduction d'un parseur de pattern (q_constr.ml4) à usage de | herbelin | 2006-03-22 |
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |