aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2005-06-28majcoq
2005-06-28Correction bug #983herbelin
2005-06-27majcoq
2005-06-26majcoq
2005-06-25majcoq
2005-06-24majcoq
2005-06-24majcoq
2005-06-24Dp: ajout d'abstraction aux applications de fonction non premier ordrecoq
2005-06-24dp: ajout des prédicats de sortescoq
2005-06-22majcoq
2005-06-22Added entry constr_may_eval for tactic extensions (new syntax)herbelin
2005-06-21majcoq
2005-06-21coqdep connait maintenant user-contribfilliatr
2005-06-20majcoq
2005-06-19majcoq
2005-06-18majcoq
2005-06-17majcoq
2005-06-16majcoq
2005-06-15majcoq
2005-06-15majcoq
2005-06-15Dp : ajoût des existentielscoq
2005-06-14majcoq
2005-06-13majcoq
2005-06-12majcoq
2005-06-11majcoq
2005-06-10majcoq
2005-06-09majcoq
2005-06-09majcoq
2005-06-09dp: traitement des fixpointscoq
2005-06-09backtrack sur le typage des instantiations d\'evarsbarras
2005-06-08majcoq
2005-06-08traitement des casecoq
2005-06-08evar declarees avec mauvais typebarras
2005-06-07majcoq
2005-06-07majcoq
2005-06-07pas de filtrages partielsbarras
2005-06-07reparations de quelques petits bugs d\'unification + introduction de la notio...barras
2005-06-06majcoq
2005-06-06essai de typage des instantiations d\'evarsbarras
2005-06-05majcoq
2005-06-05majcoq
2005-06-05eradication de Evarutil.w_Definebarras
2005-06-05assouplissement de real_clean: ne tient pas compte des occcurences flexibles ...barras
2005-06-04majcoq
2005-06-04Ajout explicite du niveau 200 de pattern auquel on fait référence au niveau...herbelin
2005-06-03majcoq
2005-06-03Prise en compte de l'utilisation des notations récursives pour faire une not...herbelin
2005-06-03suppression de code commentecoq
2005-06-03whelp + correction bug affichage de coqidecoq
2005-06-02majcoq
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-25 13:52:03 +0000