aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2005-03-19Correction erreur grossière de non restauration d'état en cas de retour exc...herbelin
2005-03-19Le type d'un Let est considéré comme 'user-provided' par le noyau et doit d...herbelin
2005-03-19Ajout test bug #935herbelin
2005-03-19Report depuis la V8.0pl2 de la correction d'un bug du traducteurherbelin
2005-03-18majcoq
2005-03-18majcoq
2005-03-18appel de Simplify depuis Coqcoq
2005-03-17majcoq
2005-03-17majcoq
2005-03-17Nouvelle syntaxe 'with' des modules non gérée en v7herbelin
2005-03-17majcoq
2005-03-17majcoq
2005-03-16majcoq
2005-03-16majcoq
2005-03-16MAJ PolyList -> Listherbelin
2005-03-16Nouvelle syntaxe 'with' des modules non gérée en v7herbelin
2005-03-16tactiques prouveurs premier ordre dans contrib/dp/coq
2005-03-16nouvelles tactiques pour appeler des procedures de decision du premier ordrecoq
2005-03-15majcoq
2005-03-15majcoq
2005-03-15Unsharing before exportation to ensure uniqueness of xml id'sherbelin
2005-03-15Backtrack sur la substitution combinée avec l'instanciation en réponse à l...herbelin
2005-03-14majcoq
2005-03-13majcoq
2005-03-12majcoq
2005-03-12Explicitation d'un nom de variable nécessaire au bon typage, suite à suppre...herbelin
2005-03-12Backtrack version 1.82 awaiting for better understanding of the consequences ...herbelin
2005-03-11majcoq
2005-03-11Méthode plus raisonnable pour supprimer l'inefficacité des evars dépendant...herbelin