| Age | Commit message (Expand) | Author |
|---|
| 2010-01-30 | Update CHANGES, add documentation for new commands/tactics and do a bit | msozeau |
| 2009-12-21 | Generic support for open terms in tactics | herbelin |
| 2009-12-12 | Updated compatibility for rewriting equality proofs that are dependent | herbelin |
| 2009-11-24 | Minor fixes in typeclasses, avoiding repeated evar normalizations. | msozeau |
| 2009-10-28 | Integrate a few improvements on typeclasses and Program from the equations br... | msozeau |
| 2009-10-21 | This big commit addresses two problems: | soubiran |
| 2009-09-17 | Remove useless Liboject.export_function field | glondu |
| 2009-09-17 | Delete trailing whitespaces in all *.{v,ml*} files | glondu |
| 2009-08-13 | Death of "survive_module" and "survive_section" (the first one was | herbelin |
| 2009-08-06 | - Cleaning phase of the interfaces of libnames.ml and nametab.ml | herbelin |
| 2009-08-06 | Move out JMeq of subst for compatibility (it affects e.g. the | herbelin |
| 2009-07-24 | Remove the barely-used/obsolete/undocumented syntax "conditional <tac> rewrite" | letouzey |
| 2009-06-30 | Add new variants of [rewrite] and [autorewrite] which differ in the | msozeau |
| 2009-05-20 | - Fixing declarative mode in presence of high use of Change_evars nodes | herbelin |
| 2009-05-09 | - Adding "Hint Resolve ->" and "Hint Resolve <-" for declaration of equivalence | herbelin |
| 2009-04-14 | Rewrite autorewrite to use a dnet indexed by the left-hand sides (or | msozeau |
| 2009-01-18 | Getting rid of the previous implementation of setoid_rewrite which was | msozeau |
| 2008-12-16 | Finish fix for the treatment of [inverse] in [setoid_rewrite], making a | msozeau |
| 2008-12-09 | About "apply in": | herbelin |
| 2008-11-05 | Port [rewrite] tactics to open terms. Currently no check that evars | msozeau |
| 2008-10-26 | Fixes and refinements regarding occurrence selection: | herbelin |
| 2008-09-25 | Various little improvements: | msozeau |
| 2008-08-04 | Évolutions diverses et variées. | herbelin |
| 2008-07-28 | Fixes in generalize_eqs/dependent induction to allow the user to specify | msozeau |
| 2008-07-22 | New tactics [conv] to test convertibility (actually, unification) of two | msozeau |
| 2008-06-21 | - Implantation de la suggestion 1873 sur discriminate. Au final, | herbelin |
| 2008-04-27 | Correction du bug des types singletons pas sous-type de Set | herbelin |
| 2008-03-06 | Plug the new setoid implemtation in, leaving the original one commented | msozeau |
| 2007-12-18 | Nettoyage de code en vue de la release. Plus de Warning: Unused | aspiwack |
| 2007-12-07 | Adding the tactic "instantiate" (without argument), to force the | glondu |
| 2007-12-05 | Factorisation des opérations sur le type option de Util dans un module | aspiwack |
| 2007-08-07 | Add a new tactic to generalize an instantiated inductive predicate adding equ... | msozeau |
| 2007-05-22 | Nouvelle stratégie d'unification des types des with-bindings dans | herbelin |
| 2007-05-20 | - Propagation des evars non résolues vers les with_bindings; permet par exemple | herbelin |
| 2007-05-11 | Processor integers + Print assumption (see coqdev mailing list for the | aspiwack |
| 2007-04-28 | Ajout de la possibilité d'utiliser les evars dans apply_in et elim_in. | herbelin |
| 2006-12-12 | Correction bug #1041 (double cause : non évitement des noms existants en | herbelin |
| 2006-10-24 | Ajout de la tactique "apply in". | herbelin |
| 2006-10-01 | Une passe sur l'injection et la discrimination... | herbelin |
| 2006-08-23 | Bug in replace tactics introduced in r9073 (overlap between replace .. with a... | jforest |
| 2006-08-22 | + Changing "in <hyp>" to "in <clause>" (no at, no InValue and no | jforest |
| 2006-06-23 | Suite utilisation hyp au lieu ident: donne la localisationn | herbelin |
| 2006-06-23 | Correction ident -> hyp pour dinterpréter des identificateurs devant êt... | herbelin |
| 2006-06-08 | Changement du type d'argument 'TacticArgType X' en un type | herbelin |
| 2006-05-30 | Généralisation de with_occurrence (ex occurrence) et de red_expr pour perme... | herbelin |
| 2006-05-02 | Extension syntaxique de rewrite in: au lieu de pouvoir faire | letouzey |
| 2006-04-27 | Standardisation nom option_app en option_map | herbelin |
| 2006-03-21 | + destruct now works as induction on multiple arguments : | jforest |
| 2006-01-21 | Messages de idtac et fail peuvent maintenant être des listes de string, int ... | herbelin |
| 2005-12-26 | Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis... | herbelin |
