aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2005-04-27majcoq
2005-04-26majcoq
2005-04-26Fixed hypotheses of Z_lt_induction (see #957)herbelin
2005-04-25majcoq
2005-04-24majcoq
2005-04-23majcoq
2005-04-22majcoq
2005-04-21majcoq
2005-04-21majcoq
2005-04-21Gestion du forall et envoie d'axiome à la procédurecoq
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-20 03:07:01 +0000