aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2005-04-21Gestion du forall et envoie d'axiome à la procédurecoq
2005-04-20majcoq
2005-04-20Implementation of a new backtracking system, that allow to go backcoq
2005-04-19majcoq
2005-04-18majcoq
2005-04-17majcoq
2005-04-16majcoq
2005-04-15majcoq
2005-04-14majcoq
2005-04-13majcoq
2005-04-12majcoq
2005-04-11majcoq
2005-04-10majcoq
2005-04-09majcoq
2005-04-08majcoq
2005-04-07majcoq
2005-04-07majcoq
2005-04-07dp: traitement des definitionscoq
2005-04-06majcoq
2005-04-05majcoq
2005-04-05Problemes de renommage reglescoq
2005-04-04majcoq
2005-04-03majcoq
2005-04-02majcoq
2005-04-01majcoq
2005-03-31majcoq
2005-03-31Added option_mapherbelin
2005-03-30majcoq
2005-03-29majcoq
2005-03-29Missing translating a 'O' into a '0' (again - cf bug #947); removed useless h...herbelin
2005-03-29Missing translating a 'O' into a '0' (again)herbelin
2005-03-28majcoq
2005-03-27majcoq
2005-03-26majcoq
2005-03-25majcoq
2005-03-24majcoq
2005-03-24majcoq
2005-03-24Missing translating a 'O' into a '0'herbelin
2005-03-24symboles de fonctions globaux traitescoq
2005-03-23majcoq
2005-03-22majcoq
2005-03-22majcoq
2005-03-22Ajout de l'axiome du but prouve par la tactique simplificoq
2005-03-21majcoq
2005-03-21Ajout Unset Implicit Arguments manquantherbelin
2005-03-20majcoq
2005-03-20Correction bug de dependent_hyps qui ne met pas à jour le type des hyps dép...herbelin
2005-03-20Test d'un bug de 'Inv.dependent_hyps' qui ne met pas à jour le type des hyps...herbelin
2005-03-19majcoq
2005-03-19majcoq