aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2005-05-19majcoq
2005-05-19Documentationherbelin
2005-05-19Déplacement de fonctionnalités unix et browser de ide vers libherbelin
2005-05-19Setoid_replace: improved error message when trying to replace a term in asacerdot
2005-05-19A wish by Bas Spitters granted: a little more of unification up tosacerdot
2005-05-19added VernacBacktrack (new backtracking command dedicated tocoq
2005-05-18majcoq
2005-05-18majcoq
2005-05-18Implemented autorewrite with ... in hyp [using ...].sacerdot
2005-05-17majcoq
2005-05-17majcoq
2005-05-17Affinements suite à extension Tactic Notation aux tacticiellesherbelin
2005-05-17Extension de Tactic Notation pour permettre d'tendre et de faire rffrence aux...herbelin
2005-05-17Extension de Tactic Notation pour permettre d'tendre et de faire rffrence aux...herbelin
2005-05-16majcoq
2005-05-15majcoq
2005-05-15majcoq
2005-05-15Globalisation des Tactic Notationherbelin
2005-05-15Allow auto to have a parametric argument (wish #967)herbelin
2005-05-15Allow auto to have a parametric argument (wish #967)herbelin
2005-05-14majcoq
2005-05-13majcoq
2005-05-12majcoq
2005-05-11majcoq
2005-05-10majcoq
2005-05-09majcoq
2005-05-09possibilité d'écrire [foo| ] au lieu de [foo|idtac]letouzey
2005-05-09possibilité d'écrire [foo| ] au lieu de [foo|idtac]letouzey
2005-05-08majcoq
2005-05-07majcoq
2005-05-06majcoq
2005-05-05majcoq
2005-05-05Bug affichage graphe universherbelin
2005-05-05Code v7 obsoleteherbelin
2005-05-05MAJ commentaires et inversion du sens du graphe de contraintes pour extensibi...herbelin
2005-05-04majcoq
2005-05-03majcoq
2005-05-03Open Scope non Local malencontreuxherbelin
2005-05-02majcoq
2005-05-02Finalement, préservation de la compatibilité pour Z_lt_induction et ajout p...herbelin
2005-05-02Lemme de passage de l'autre côté d'une égalitéherbelin
2005-05-02Utilisation Z_scopeherbelin
2005-05-01majcoq
2005-04-30majcoq
2005-04-29majcoq
2005-04-29Protection against saving a proof with still non-instantiated evars (cf bug #...herbelin
2005-04-29Protection against saving a proof with still non-instantiated evars (cf bug #...herbelin
2005-04-29Improved order of interpretation of atomic tactics (cf bug #952)herbelin
2005-04-29Fix bug in prepare_predicate_from_tycon; improved error message when no claus...herbelin
2005-04-28majcoq
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-03 05:49:56 +0000